Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002504Frama-CKernelpublic2020-03-26 10:252020-05-07 09:27
Reporterjens 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C 20-Calcium 
Target VersionFixed in Version 
Summary0002504: more precise error message for missing closing } of axiomatic block
DescriptionThe 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.
TagsNo tags attached.
Attached Filesc file icon ax.c [^] (68 bytes) 2020-03-26 10:25 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2020-03-26 10:25 jens New Issue
2020-03-26 10:25 jens File Added: ax.c
2020-05-07 09:27 maroneze Assigned To => virgile
2020-05-07 09:27 maroneze Status new => acknowledged


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker