Frama-C Bug Tracking System - Frama-C
View Issue Details
0002127Frama-CPlug-in > wppublic2015-06-04 11:502016-01-26 08:43
loic 
correnson 
normalminoralways
closedfixed 
LinuxUbuntu12.04.5 LTS
 
Frama-C Magnesium 
0002127: Unprovable inequality involving (unsigned) -1
Nitrogen-20111001 alt-ergo 0.94 The following assertion cannot be proven. void arithmetic_testcase(unsigned i) { /*@ assert i <= (unsigned) -10 ==> i + 9 <= (unsigned) -1; */ }
frama-c -wp -wp-ret for the code above (also as attachment).
No tags attached.
c arithmetic_testcase.c (164) 2015-06-04 11:50
https://bts.frama-c.com/file_download.php?file_id=1042&type=bug
Issue History
2015-06-04 11:50loicNew Issue
2015-06-04 11:50loicStatusnew => assigned
2015-06-04 11:50loicAssigned To => correnson
2015-06-04 11:50loicFile Added: arithmetic_testcase.c
2015-06-29 16:37corrensonNote Added: 0005950
2015-06-29 16:38corrensonStatusassigned => closed
2015-06-29 16:38corrensonResolutionopen => fixed
2015-06-29 16:38corrensonFixed in Version => Frama-C Magnesium
2015-06-29 16:42corrensonStatusclosed => resolved
2016-01-26 08:43signolesStatusresolved => closed

Notes
(0005950)
correnson   
2015-06-29 16:37   
Proved by Qed.