|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0000088||Frama-C||Kernel||public||2009-05-19 17:45||2014-02-12 16:56|
|Product Version||Frama-C Lithium-20081201|
|Target Version||Fixed in Version||Frama-C Beryllium-20090601-beta1|
|Summary||0000088: 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.
|Tags||No tags attached.|
|This seems quite a good idea. The legitimate use is mostly historical anyway.|
|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.|
|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.|
|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||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|