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.
|Fixed in Version
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.