2021-02-24 18:44 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002127Frama-CPlug-in > wppublic2015-06-04 11:502016-01-26 08:43
Reporterloic 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformLinuxOSUbuntuOS Version12.04.5 LTS
Product Version 
Target VersionFixed in VersionFrama-C Magnesium 
Summary0002127: Unprovable inequality involving (unsigned) -1
DescriptionNitrogen-20111001
alt-ergo 0.94

The following assertion cannot be proven.

void arithmetic_testcase(unsigned i) {
    /*@ assert i <= (unsigned) -10 ==> i + 9 <= (unsigned) -1; */
}
Steps To Reproduceframa-c -wp -wp-ret for the code above (also as attachment).
TagsNo tags attached.
Attached Files
  • c file icon arithmetic_testcase.c (164 bytes) 2015-06-04 11:50 - 
    /* frama-c -wp -wp-rte   */
/* alt-ergo version 0.94 */

void arithmetic_testcase(unsigned i) {
    /*@ assert i <= (unsigned) -10 ==> i + 9 <= (unsigned) -1; */
}
    c file icon arithmetic_testcase.c (164 bytes) 2015-06-04 11:50 +

-Relationships
+Relationships

-Notes

~0005950

correnson (manager)

2015-06-29 16:37

 Proved by Qed.
+Notes

-Issue History
Date Modified Username Field Change
2015-06-04 11:50 loic New Issue
2015-06-04 11:50 loic Status new => assigned
2015-06-04 11:50 loic Assigned To => correnson
2015-06-04 11:50 loic File Added: arithmetic_testcase.c
2015-06-29 16:37 correnson Note Added: 0005950
2015-06-29 16:38 correnson Status assigned => closed
2015-06-29 16:38 correnson Resolution open => fixed
2015-06-29 16:38 correnson Fixed in Version => Frama-C Magnesium
2015-06-29 16:42 correnson Status closed => resolved
2016-01-26 08:43 signoles Status resolved => closed
+Issue History