suggest to supply lower-bound for constant_too_large_2147483647 to Simplify
ID0001008: This issue was created automatically from Mantis Issue 1008. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001008 | Frama-C | Plug-in > jessie | public | 2011-11-03 | 2011-11-16 |
| Reporter | Jochen | Assigned To | cmarche | Resolution | open |
| Priority | normal | Severity | feature | Reproducibility | N/A |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | - |
Description :
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.