Frama-C Bug Tracking System - Frama-C
View Issue Details
0001008Frama-CPlug-in > jessiepublic2011-11-03 18:532011-11-16 14:03
Jochen 
cmarche 
normalfeatureN/A
assignedopen 
Frama-C Nitrogen-20111001 
 
0001008: suggest to supply lower-bound for constant_too_large_2147483647 to Simplify
Simplify'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.
No tags attached.
? pgm.sx (26,964) 2011-11-03 18:53
https://bts.frama-c.com/file_download.php?file_id=289&type=bug
c ftest.c (141) 2011-11-16 13:59
https://bts.frama-c.com/file_download.php?file_id=295&type=bug
Issue History
2011-11-03 18:53JochenNew Issue
2011-11-03 18:53JochenStatusnew => assigned
2011-11-03 18:53JochenAssigned To => cmarche
2011-11-03 18:53JochenFile Added: pgm.sx
2011-11-08 07:37monateNote Added: 0002456
2011-11-16 13:59JochenFile Added: ftest.c
2011-11-16 14:03JochenNote Added: 0002474

Notes
(0002456)
monate   
2011-11-08 07:37   
@Claude: wouldn't it be a nice feature request for Why itself?
(0002474)
Jochen   
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.