Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000779Frama-CPlug-in > wppublic2011-04-08 16:052011-10-10 14:14
Reporterpatrick 
Assigned Todargaye 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20101202-beta2 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000779: Hypothesis missing about pointed datatypes
DescriptionAn hypothesis about the bounds of the pointed data seems to be missing.
The assertion of the given example cannot be proved with WP Carbon beta-2.

file pb_uint8.c
---------------
void f(unsigned char *t) {
//@ assert t[0] < 256;
        t[1]=3;
}

command: frama-c-gui -wp -wp-axioms pb_uint8.c
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2011-04-08 16:05 patrick New Issue
2011-04-08 16:05 patrick Status new => assigned
2011-04-08 16:05 patrick Assigned To => dargaye
2011-05-27 14:27 dargaye Status assigned => resolved
2011-05-27 14:27 dargaye Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker