|View Issue Details [ Jump to Notes ] ||[ Issue History ] [ Print ] |
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0000433||Frama-C||Plug-in > jessie||public||2010-03-22 17:28||2010-03-23 15:02|
|Assigned To||virgile|| |
|Product Version||Frama-C Beryllium-20090902|| |
|Target Version||Fixed in Version|| |
|Summary||0000433: different translation of casted constants in program-code and in assertion|
|Description||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.|
|Tags||No tags attached.|
|Attached Files|| ftest.c [^] (136 bytes) 2010-03-22 17:28 [Show Content]