GitLab

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

---

Id	Project	Category	View	Due Date	Updated
ID0002021	Frama-C	Documentation > ACSL	public	2014-12-05	2016-01-26

Reporter	gaggarwal	Assigned To	patrick	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Neon-20140301	Target Version	-	Fixed in Version	Frama-C Magnesium

Description :

Grammar for loop-behavior in Fig2.9 in acsl.pdf (http://frama-c.com/download/acsl.pdf), page 36, has bug. loop-behavior has following grammar:

    loop-behavior := for id (, id)* : loop-clause*

which means that having atleast one loop clause is not necessary. But if I don't add any loop-clause frama-c throws warning: unexpected token ' ' in line XX

Steps To Reproduce :

Following example is correct as per the grammar of loop-behavior. But frama-c throws warning.

/*@ requires n>=0; behavior fail : ensures \result == -1; / int example(double t[], int n, double v ){ int l=0, u= n-1; /@ loop invariant 0 <=l && u <= n-1; for fail: */
while(l <= u){ l++; } return -1; }

Note: this is contrived example