2021-03-02 03:03 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000095Frama-CPlug-in > jessiepublic2009-06-23 18:03
Reportermottainai 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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 
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-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
+Issue History