Frama-C Bug Tracking System - Frama-C
View Issue Details
0002504Frama-CKernelpublic2020-03-26 10:252020-03-26 10:25
jens 
 
normalminoralways
newopen 
Frama-C 20-Calcium 
 
0002504: more precise error message for missing closing } of axiomatic block
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.
No tags attached.
c ax.c (68) 2020-03-26 10:25
https://bts.frama-c.com/file_download.php?file_id=1349&type=bug
Issue History
2020-03-26 10:25jensNew Issue
2020-03-26 10:25jensFile Added: ax.c

There are no notes attached to this issue.