Frama-C Bug Tracking System - Frama-C
View Issue Details
0000095Frama-CPlug-in > jessiepublic2009-05-25 14:462009-06-23 18:03
Assigned Tocmarche 
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
TagsNo tags attached.
related to 0000094closed cmarche "assert i >= 0;" not proven for unsigned char 
Attached Files

There are no notes attached to this issue.

Issue History
2009-05-25 14:46mottainaiNew Issue
2009-05-25 16:02signolesStatusnew => assigned
2009-05-25 16:02signolesAssigned To => cmarche
2009-05-25 16:02signolesRelationship addedrelated to 0000094
2009-06-18 16:48cmarcheStatusassigned => resolved
2009-06-18 16:48cmarcheResolutionopen => fixed
2009-06-23 18:02signolesStatusresolved => closed
2009-06-23 18:03signolesFixed in Version => Frama-C Beryllium beta-1