-2147483647<=0 unprovable by Simplify, except in switch
ID0000415: This issue was created automatically from Mantis Issue 415. Further discussion may take place here.
|ID0000415||Frama-C||Plug-in > jessie||public||2010-02-22||2010-03-30|
|Reporter||Jochen||Assigned To||cmarche||Resolution||no change required|
|Product Version||Frama-C Beryllium-20090902||Target Version||-||Fixed in Version||-|
Simplify can prove neither -2147483648<=0 nor -2147483647<=0, see ftest8() and ftest7() in the attached file. However, it proves -2147483646<=0, see ftest6(). I suggest a jessie cmd-line option to generate -2147483646 rather than -2147483648 as MinInt, in order to circumvent this bug of Simplify, which causes many unprovable no-underflow-obligations in my programs.
Moreover, as a case of a switch, Simplify behaves different on -2147483647<=0: it can prove it there, see case 7 in ftest(). Probably, this is again a problem of Simplify. To ensure this, you could check that the proof obligations you generate are correct.