Frama-C Bug Tracking System - Frama-C |
| View Issue Details |
|
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0000512 | Frama-C | Kernel | public | 2010-06-17 18:18 | 2014-02-12 16:55 |
|
| Reporter | Jochen | |
|---|
| Assigned To | virgile | |
|---|
| Priority | normal | Severity | trivial | Reproducibility | always |
|---|
| Status | closed | Resolution | fixed | |
|---|
| Platform | | OS | | OS Version | |
|---|
| Product Version | Frama-C Boron-20100401 | |
|---|
| Target Version | | Fixed in Version | Frama-C Carbon-20101201-beta1 | |
|---|
|
| Summary | 0000512: suggest to refer to fct-contract's clauses-order in error message |
|---|
| 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. |
|---|
| Tags | No tags attached. |
|---|
| Relationships | |
| Attached Files | |
|---|