Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000094Frama-CPlug-in > jessiepublic2009-05-25 14:402009-06-23 18:03
Reportermottainai 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Lithium-20081201 
Target VersionFixed in VersionFrama-C Beryllium-20090601-beta1 
Summary0000094: "assert i >= 0;" not proven for unsigned char
DescriptionThe 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;
}
Additional InformationI am using Frama-C Lithium-20081201 on Mac OS X 10.5.7
TagsNo tags attached.
Attached Files

- Relationships
related to 0000095closedcmarche "//@ assert i >= CHAR_MIN;" not proven for char 

-  Notes
(0000094)
signoles (manager)
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 [^]

- Issue History
Date Modified Username Field Change
2009-05-25 14:40 mottainai New Issue
2009-05-25 16:01 signoles Status new => assigned
2009-05-25 16:01 signoles Assigned To => cmarche
2009-05-25 16:01 signoles Note Added: 0000094
2009-05-25 16:01 signoles Status assigned => confirmed
2009-05-25 16:02 signoles Relationship added related to 0000095
2009-06-18 14:57 cmarche Status confirmed => resolved
2009-06-18 14:57 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