axiom ignored because of label, but no label is present in axiom.

ID0000576: This issue was created automatically from Mantis Issue 576. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000576	Frama-C	Plug-in > wp	public	2010-08-26	2014-02-12

Reporter	derepas	Assigned To	Anne	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C GIT, precise the release id	Target Version	-	Fixed in Version	Frama-C Nitrogen-20111001

Description :

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.