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.
|Product Version||Frama-C 20-Calcium||Target Version||-||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.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information