# 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.