Closed
Description
The following program:
public class short2
{
short a;
void f()
{
a++;
}
}
fails with
converting SSA
+
* type: signedbv
* width: 16
0: byte_extract_little_endian
* type: signedbv
* width: 16
0: symbol
* type: empty
* identifier: tmp_object_factory$1!0#1
* expression: symbol
* type: empty
* identifier: tmp_object_factory$1
* L0: 0
* L2: 1
* #SSA_symbol: 1
1: constant
* type: signedbv
* width: 64
* #c_type: signed_long_int
* value: 0000000000000000000000000000000000000000000000000000000000000100
1: constant
* type: signedbv
* width: 32
* #c_type: signed_int
* value: 00000000000000000000000000000001
add/sub with mixed types
when using cbmc --cover location --function short2.f short2.class