Frama-C Bug Tracking System - Frama-C
View Issue Details
0000779Frama-CPlug-in > wppublic2011-04-08 16:052011-10-10 14:14
patrick 
dargaye 
normalminoralways
closedfixed 
Frama-C Carbon-20101202-beta2 
Frama-C Nitrogen-20111001 
0000779: Hypothesis missing about pointed datatypes
An 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
No tags attached.
Issue History
2011-04-08 16:05patrickNew Issue
2011-04-08 16:05patrickStatusnew => assigned
2011-04-08 16:05patrickAssigned To => dargaye
2011-05-27 14:27dargayeStatusassigned => resolved
2011-05-27 14:27dargayeResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed

There are no notes attached to this issue.