more precise error message for missing closing } of axiomatic block
ID0002504: This issue was created automatically from Mantis Issue 2504. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002504 | Frama-C | Kernel | public | 2020-03-26 | 2020-05-07 |
| Reporter | jens | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C 20-Calcium | Target Version | - | Fixed in Version | - |
Description :
The attached example lacks the closing '}' of the axiomatic block. Frama-C's error message says
[kernel:annot-error] ax.c:5: Warning: unexpected token ''
In a more complex setting I have spent some time to figure out what is wrong in line 5 (where 'bar' is defined).
A more precise error message that explicitly mentions the axiomatic block would be helpful.