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.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000433 | Frama-C | Plug-in > jessie | public | 2010-03-22 | 2010-03-23 |
| Reporter | Jochen | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | tweak | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Beryllium-20090902 | Target Version | - | Fixed in Version | - |
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.