Closed
Description
The following fails with cbmc --cover location --function bitwise1.f bitwise1.class with the above error.
public class bitwise1
{
static char c;
void f()
{
int i = (c & 2);
}
}
In boolbvt_bitwise::convert_bitwise the reported width of the char operand is 16 (from std::size_t width=boolbv_width(expr.type());) but the size of the converted operand is 32. Java uses widening numeric promotion to int in this case. Interestingly, this program does not produce the above error in the following version (1 instead of 2):
public class bitwise1
{
static char c;
void f()
{
int i = (c & 1);
}
}