Frama-C Bug Tracking System - Frama-C
View Issue Details
0000092Frama-CPlug-in > jessiepublic2009-05-20 18:452009-06-19 09:07
virgile 
cmarche 
normalminoralways
assignedreopened 
Frama-C Lithium-20081201 
 
0000092: Why error with logic functions returning a pointer
The following code (a stripped down example of the bug reported by Alan Dunn on the mailing list: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-May/001151.html) gives an erroneous Why file when analyzed with frama-c -jessie-analysis file.c Either jessie should exit with an appropriate error message, or the why compilation should succeed. char T; /*@ axiomatic foo { logic char* foo{L}(integer x) = &T; } */ /*@ predicate strcmp{L}(char *x, char* y) = \forall integer i; (\forall integer j; 0<=j *(x+j) !=0) ==> *(x+i) == *(y+i); */
No tags attached.
Issue History
2009-05-20 18:45virgileNew Issue
2009-05-25 16:20signolesStatusnew => assigned
2009-05-25 16:20signolesAssigned To => cmarche
2009-05-25 16:20signolesStatusassigned => confirmed
2009-06-18 16:56cmarcheStatusconfirmed => resolved
2009-06-18 16:56cmarcheResolutionopen => unable to reproduce
2009-06-18 17:46virgileNote Added: 0000197
2009-06-18 17:46virgileStatusresolved => feedback
2009-06-18 17:46virgileResolutionunable to reproduce => reopened
2009-06-19 09:07cmarcheStatusfeedback => assigned

Notes
(0000197)
virgile   
2009-06-18 17:46   
For some reason, the code snippet that reproduces the bug was cut in the description. For the bug to appear, the foo logic function must be used, e.g. in the following specification of function f: /*@ ensures strcmp(foo(x),foo(\result)); */ int f(int x) { return x++; }