Frama-C Bug Tracking System - Frama-C
View Issue Details
0000433Frama-CPlug-in > jessiepublic2010-03-22 17:282010-03-23 15:02
Jochen 
virgile 
normaltweakalways
assignedopen 
Frama-C Beryllium-20090902 
 
0000433: different translation of casted constants in program-code and in assertion
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.
No tags attached.
c ftest.c (136) 2010-03-22 17:28
https://bts.frama-c.com/file_download.php?file_id=71&type=bug
Issue History
2010-03-22 17:28JochenNew Issue
2010-03-22 17:28JochenStatusnew => assigned
2010-03-22 17:28JochenAssigned To => cmarche
2010-03-22 17:28JochenFile Added: ftest.c
2010-03-23 15:02signolesAssigned Tocmarche => virgile

There are no notes attached to this issue.