different translation of casted constants in program-code and in assertion
ID0000433: This issue was created automatically from Mantis Issue 433. Further discussion may take place here.
|ID0000433||Frama-C||Plug-in > jessie||public||2010-03-22||2010-03-23|
|Product Version||Frama-C Beryllium-20090902||Target Version||-||Fixed in Version||-|
In the attached file, "my_const" is translated to "1024" in line 8 (C-code), but to "integer_of_int32(int32_of_integer(1024))" in line 9 (Acsl-code).
As a consequence, Simplify is unable to prove the trivial-looking assertion in line 9 (it seems to lack a rule like "integer_of_int32(int32_of_integer(x)) <== -maxInt <= x <= +maxInt").
When I remove the cast in line 4, jessie outputs no proof obligation at all, which is (consistent with) what I expected.