2021-01-15 15:51 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000779Frama-CPlug-in > wppublic2011-10-10 14:14
Assigned Todargaye 
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;

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


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
+Issue History