Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000095Frama-CPlug-in > jessiepublic2009-05-25 14:462009-06-23 18:03
Reportermottainai 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Lithium-20081201 
Target VersionFixed in VersionFrama-C Beryllium-20090601-beta1 
Summary0000095: "//@ assert i >= CHAR_MIN;" not proven for char
DescriptionThe first assertion in the the following code fragment is not proven.
(neither alt-ergo nor yices nor cvc3).

char char_range(char i)
{
    //@ assert i >= CHAR_MIN;
    //@ assert i <= CHAR_MAX;
    return i;
}
Additional InformationI am using Frama-C Lithium-20081201 on Mac OS X 10.5.7
This is probably related to bug http://bts.frama-c.com/view.php?id=94 [^]
TagsNo tags attached.
Attached Files

- Relationships
related to 0000094closedcmarche "assert i >= 0;" not proven for unsigned char 

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2009-05-25 14:46 mottainai New Issue
2009-05-25 16:02 signoles Status new => assigned
2009-05-25 16:02 signoles Assigned To => cmarche
2009-05-25 16:02 signoles Relationship added related to 0000094
2009-06-18 16:48 cmarche Status assigned => resolved
2009-06-18 16:48 cmarche Resolution open => fixed
2009-06-23 18:02 signoles Status resolved => closed
2009-06-23 18:03 signoles Fixed in Version => Frama-C Beryllium beta-1


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker