Frama-C Bug Tracking System - Frama-C
View Issue Details
0000095Frama-CPlug-in > jessiepublic2009-05-25 14:462009-06-23 18:03
mottainai 
cmarche 
normalminoralways
closedfixed 
Frama-C Lithium-20081201 
Frama-C Beryllium-20090601-beta1 
0000095: "//@ assert i >= CHAR_MIN;" not proven for char
The 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; }
I 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
No tags attached.
related to 0000094closed cmarche "assert i >= 0;" not proven for unsigned char 
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

There are no notes attached to this issue.