2021-01-15 15:23 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002504Frama-CKernelpublic2020-05-07 09:27
Reporterjens 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
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 Files
  • c file icon ax.c (68 bytes) 2020-03-26 10:25 -
    /*@
      axiomatic foo
      {
        logic integer bar(integer i) = i+1;
    */
    
    c file icon ax.c (68 bytes) 2020-03-26 10:25 +

-Relationships
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-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
+Issue History