Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000433Frama-CPlug-in > jessiepublic2010-03-22 17:282010-03-23 15:02
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeveritytweakReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in Version 
Summary0000433: different translation of casted constants in program-code and in assertion
DescriptionIn 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.
TagsNo tags attached.
Attached Filesc file icon ftest.c [^] (136 bytes) 2010-03-22 17:28 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2010-03-22 17:28 Jochen New Issue
2010-03-22 17:28 Jochen Status new => assigned
2010-03-22 17:28 Jochen Assigned To => cmarche
2010-03-22 17:28 Jochen File Added: ftest.c
2010-03-23 15:02 signoles Assigned To cmarche => virgile


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker