Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000088Frama-CKernelpublic2009-05-19 17:452014-02-12 16:56
Reporterdmentre 
Assigned Tovirgile 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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
DescriptionHello,

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.

Yours,
david
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000078)
monate (reporter)
2009-05-20 00:33

This seems quite a good idea. The legitimate use is mostly historical anyway.
(0000079)
virgile (developer)
2009-05-20 15:13

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.
(0000082)
dmentre (reporter)
2009-05-20 18:16

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 Checkin
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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker