suggest to refer to fct-contract's clauses-order in error message
ID0000512: This issue was created automatically from Mantis Issue 512. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000512 | Frama-C | Kernel | public | 2010-06-17 | 2014-02-12 |
| Reporter | Jochen | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | trivial | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | Frama-C Carbon-20101201-beta1 |
Description :
If the clauses-order (specified in Fig.2.4 (p.27) of the document "ACSL Version 1.4 / Implementation in Boron-20100401") is violated by a program, the kernel just reports "user error: syntax error while parsing annotation". I suggest to replace that rather general message by a more specific like e.g. "decreases-clause after ensures-clauses not allowed in function contract".
Similarly, a message like "decreases-clause missing for recursive function" rather than tacitly generating an unsatisfiable proof goal "... ==> 0<0" would be helpful.