Frama-C Bug Tracking System

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 Filesc file icon arithmetic_testcase.c [^] (164 bytes) 2015-06-04 11:50 [Show Content]

- Relationships

-  Notes
(0005950)
correnson (manager)
2015-06-29 16:37

Proved by Qed.

- 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


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker