order of 'decreases' and 'behavior' clauses

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

---

Id	Project	Category	View	Due Date	Updated
ID0000327	Frama-C	Kernel > ACSL implementation	public	2009-11-10	2010-04-13

Reporter	cmarche	Assigned To	virgile	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	-	Target Version	-	Fixed in Version	Frama-C Boron-20100401

Description :

The ACSL grammar specifies that function contracts have the form

function-contract ::= simple-behavior named-behavior* decreases-clause?

however, Frama-C accepts the following without giving any errors nor warnings, and silently ignores the behaviors.

I think that the camlyacc parser should look for the "EOF" terminator of specs to prevent from silently ignore erroneous garbage.

By the way, I think that decreases clauses should be accepted also between requires and behaviors. The reason is that 'decreases t' refer to the value of t in the pre-state, and it seems more natural to me to put clauses realted to the pre-state before those related to the post-state.

/@ decreases 101-n ; @ behavior less_than_101: @ assumes n <= 100; @ ensures \result == 91; @ behavior greater_than_100: @ assumes n >= 101; @ ensures \result == n - 10; @/ int f91(int n) { if (n <= 100) { return f91(f91(n + 11)); } else return n - 10; }

Additional Information :

Pour preciser ma pensee concernant ocamlyacc et logic_parser.mly: l'entree "annot" a la forme

annot: annotation EOF

et je pense que les autres entrees de la grammaire, lexpr et spec, devraient subir le meme traitement.