2021-03-02 03:12 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000088Frama-CKernelpublic2014-02-12 16:56
Assigned Tovirgile 
Product VersionFrama-C Lithium-20081201 
Target VersionFixed in VersionFrama-C Beryllium-20090601-beta1 
Summary0000088: Frama-C should stop on error in annotations instead of issuing a warning

Currently, Frama-C is issuing a warning if there is a typo in an annotation and ignores the annotation.

Typically once have:
File jenn-issue.c, line 13, characters 55-56:
Error during analysis of annotation: unbound logic variable k
jenn-issue.c:13: Warning: ignoring logic code annotation

I think this issue is source of errors and further issues for the user.

Instead, Frama-C should stop processing the file and issue a fatal error.

Of course, one could add a command line option to restore current behaviour for legitimate(?) use.

TagsNo tags attached.
Attached Files




monate (reporter)

This seems quite a good idea. The legitimate use is mostly historical anyway.


virgile (developer)

In the mean time, note that a workaround is to launch frama-c with all analyses off, thus having only the result of type-checking on the output.


dmentre (reporter)

Thank you Virgile. I already used that approach to check my annotations, useful when you have a lot of them. But my remark was more to have a structural response to a recurring issue, as witnessed on the frama-c mailing list.

-Issue History
Date Modified Username Field Change
2009-05-19 17:45 dmentre New Issue
2009-05-20 00:33 monate Note Added: 0000078
2009-05-20 00:34 monate Assigned To => monate
2009-05-20 00:34 monate Status new => acknowledged
2009-05-20 15:13 virgile Note Added: 0000079
2009-05-20 18:16 dmentre Note Added: 0000082
2009-06-05 18:36 virgile Status acknowledged => assigned
2009-06-05 18:36 virgile Assigned To monate => virgile
2009-06-08 17:05 svn
2009-06-08 17:05 svn Status assigned => resolved
2009-06-08 17:05 svn Resolution open => fixed
2009-06-23 18:02 signoles Status resolved => closed
2009-06-23 18:03 signoles Fixed in Version => Frama-C Beryllium beta-1
2013-12-19 01:13 Source_changeset_attached => framac master ef03f1d2
2014-02-12 16:56 Source_changeset_attached => framac stable/neon ef03f1d2
+Issue History