Frama-C should stop on error in annotations instead of issuing a warning
ID0000088: This issue was created automatically from Mantis Issue 88. Further discussion may take place here.
|Fixed in Version
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.