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. ## Attachments - [pgm.sx](/uploads/461ecdb5eacd4de0ffb5cecd7e9a58da/pgm.sx) - [ftest.c](/uploads/b03bac09f0319487e3ac7e8a2bcfe453/ftest.c)