Frama-C Bug Tracking System - Frama-C
View Issue Details
0000576Frama-CPlug-in > wppublic2010-08-26 11:112014-02-12 16:55
derepas 
Anne 
normalminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Nitrogen-20111001 
0000576: axiom ignored because of label, but no label is present in axiom.
svn release id is 'r9704'. I have the following code in file ex.c: /*@ @ axiomatic MyAxio { @ logic integer my_super_fun (char * x,char * y); @ axiom my_super_axiom_1: \forall char* x; \forall char* y; @ (*(x+0)==*(y+0)) ==> my_super_fun(x,y); @ axiom my_super_axiom_2: \forall char * x; \forall char * y; @ (x[0]==y[0]) ==> my_super_fun(x,y); @ } @*/ int main (char *x, char *y) { //@ assert my_super_fun (x,y); return 0; } Launching the wp on this code yields : > frama-c -wp -wp-out why_dir ex.c [kernel] preprocessing with "gcc -C -E -I. ex.c" ex.c:11:[wp] warning: Ignoring axiom my_super_axiom_2 (because of labels) ex.c:11:[wp] warning: Ignoring axiom my_super_axiom_1 (because of labels) But it seems to me that there are no labels in these axioms.
No tags attached.
Issue History
2010-08-26 11:11derepasNew Issue
2010-08-26 11:11derepasStatusnew => assigned
2010-08-26 11:11derepasAssigned To => Anne
2010-08-26 11:15AnneNote Added: 0001103
2010-08-26 11:16AnneRelationship addedchild of 0000573
2010-08-26 11:25derepasNote Added: 0001104
2010-08-26 11:50AnneStatusassigned => resolved
2010-08-26 11:50AnneResolutionopen => no change required
2010-08-26 13:58signolesStatusresolved => closed
2011-04-04 09:30svnCheckin
2011-04-04 09:30svnNote Added: 0001682
2011-04-04 09:30svnStatusclosed => resolved
2011-04-04 09:30svnResolutionno change required => fixed
2011-04-04 09:55signolesNote Deleted: 0001682
2011-04-04 09:56signolesStatusresolved => closed
2011-04-04 10:04svnCheckin
2011-04-04 10:04svnStatusclosed => resolved
2011-04-13 15:28signolesNote Added: 0001769
2011-04-13 15:28signolesFixed in Version => Frama-C Carbon-20110201
2011-04-13 15:28signolesStatusresolved => closed
2011-09-30 12:35corrensonNote Added: 0002359
2011-09-30 12:35corrensonStatusclosed => resolved
2011-10-10 14:13signolesFixed in VersionFrama-C Carbon-20110201 => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed

Notes
(0001103)
Anne   
2010-08-26 11:15   
In fact, there is an implicit label in the logic function definition because it has pointer parameters, so it needs a memory state to be evaluated. So the axioms have a label too.
(0001104)
derepas   
2010-08-26 11:25   
Thank you for the explanation !
(0001769)
signoles   
2011-04-13 15:28   
Fixed in WP 0.3 compatible with Frama-C Carbon.
(0002359)
correnson   
2011-09-30 12:35   
Parent bug.