Frama-C Bug Tracking System - Frama-C
View Issue Details
0000094Frama-CPlug-in > jessiepublic2009-05-25 14:402009-06-23 18:03
mottainai 
cmarche 
normalminoralways
closedfixed 
Frama-C Lithium-20081201 
Frama-C Beryllium-20090601-beta1 
0000094: "assert i >= 0;" not proven for unsigned char
The first assertion in the the following code fragment is not proven. (neither alt-ergo nor yices nor cvc3). unsigned char uchar_range(unsigned char i) { //@ assert i >= 0; //@ assert i <= UCHAR_MAX; return i; }
I am using Frama-C Lithium-20081201 on Mac OS X 10.5.7
No tags attached.
related to 0000095closed cmarche "//@ assert i >= CHAR_MIN;" not proven for char 
Issue History
2009-05-25 14:40mottainaiNew Issue
2009-05-25 16:01signolesStatusnew => assigned
2009-05-25 16:01signolesAssigned To => cmarche
2009-05-25 16:01signolesNote Added: 0000094
2009-05-25 16:01signolesStatusassigned => confirmed
2009-05-25 16:02signolesRelationship addedrelated to 0000095
2009-06-18 14:57cmarcheStatusconfirmed => resolved
2009-06-18 14:57cmarcheResolutionopen => fixed
2009-06-23 18:02signolesStatusresolved => closed
2009-06-23 18:03signolesFixed in Version => Frama-C Beryllium beta-1

Notes
(0000094)
signoles   
2009-05-25 16:01   
Confirmed by Claude on the Frama-c-discuss mailing list: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-May/001187.html