Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001008Frama-CPlug-in > jessiepublic2011-11-03 18:532011-11-16 14:03
ReporterJochen 
Assigned Tocmarche 
PrioritynormalSeverityfeatureReproducibilityN/A
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in Version 
Summary0001008: suggest to supply lower-bound for constant_too_large_2147483647 to Simplify
DescriptionSimplify's problems with proving bounds of int values are well-known. E.g. for the program «int ftest(short s){return s;}», Simplify can't prove the obvious fact that the value s fits into the int type range [-2147483648..2147483647]. A reason is that the range bounds had to be modeled by abstract constants in order to prevent Simplify from crashing. I suggest to add by default an axiom "2147450877 < constant_too_large_2147483647 < constant_too_large_2147483648", in order to provide the sharpest bound possible without crashing Simplify. (A bound "2147450878" already causes a crash.)

Without such an axiom, there is no information about the size of those constants at all!

With that axiom (line 11-14 in the attached file pgm.sx), Simplify proves the above type-fit obligation, and hopefully numerous similar obligations.
TagsNo tags attached.
Attached Files? file icon pgm.sx [^] (26,964 bytes) 2011-11-03 18:53
c file icon ftest.c [^] (141 bytes) 2011-11-16 13:59 [Show Content]

- Relationships

-  Notes
(0002456)
monate (reporter)
2011-11-08 07:37

@Claude: wouldn't it be a nice feature request for Why itself?
(0002474)
Jochen (reporter)
2011-11-16 14:03

As a work-around, a clause "requires 2147450877<2147483647<2147483648" can be used on Acsl level; cf. the attached file ftest.c which is verified only with such a clause.

- Issue History
Date Modified Username Field Change
2011-11-03 18:53 Jochen New Issue
2011-11-03 18:53 Jochen Status new => assigned
2011-11-03 18:53 Jochen Assigned To => cmarche
2011-11-03 18:53 Jochen File Added: pgm.sx
2011-11-08 07:37 monate Note Added: 0002456
2011-11-16 13:59 Jochen File Added: ftest.c
2011-11-16 14:03 Jochen Note Added: 0002474


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker