the documented grammar does not allow completeness clauses in statement contracts

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

---

Id	Project	Category	View	Due Date	Updated
ID0002224	Frama-C	Documentation > ACSL	public	2016-04-13	2016-12-05

Reporter	DavidCok	Assigned To	patrick	Resolution	fixed
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Magnesium	Target Version	-	Fixed in Version	-

Description :

the documented grammar does not allow completeness clauses in statement contracts, but Frama-C wp does. I presume the implemented behavior is what is desired, so then the documentation should be updated.