Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001388Frama-CKernelpublic2013-04-11 11:372014-03-13 15:57
Reporteryakobowski 
Assigned Tosignoles 
PrioritylowSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFrama-C Neon-20140301Fixed in VersionFrama-C Neon-20140301 
Summary0001388: Frama-C should not honor -save if when it aborts
DescriptionThis is problematic because it complicates the use of Makefile. Typical pattern:

Makefile:
foo.sav: $(DEPS)
  frama-c <options> -save $@

make foo.sav
<Frama-C aborts on an user or something else>
<change something to your configuration/plugin/etc>
make foo.sav
make: `foo.sav' is up to date.

Frama-c not creating a foo.sav on the first invocation would solve the problem. What do you think? Are there some good cases when dumping partial saves is useful? In fact, what do those saves contain, since at least one plugin failed. Is the internal state really consistent?
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0003787)
signoles (manager)
2013-04-11 13:22

Actually whether the state is consistent depends on when Frama-C aborts: either the saved state is the last consistent one, or it is at least partially inconsistent. In the former case, it may be really useful for debugging. Even in the latter case, it could be useful depending on the status of the inconsistency.

So I understand your issue but, since the state may be useful, I'm not sure it is a good idea to prevent saving anytime Frama-C fails. Maybe we could adopt the following classification:
- on normal exit: save (of course)
- on Sys.break, system error, user error or feature request: do not save
- on fatal error or unexpected error: save, but slighly change the generated filename [f.sav] to [f.crash.sav] or something similar.

What do you think of this proposal?
(0003788)
yakobowski (manager)
2013-04-11 13:41

Great idea. This is much neater, and will indeed not cause problems with debugging.
(0003789)
signoles (manager)
2013-04-11 14:04
edited on: 2013-04-11 14:04

Will be implemented. Hopefully it is not Fluorine-critical...

(0004571)
signoles (manager)
2014-02-12 16:58

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2013-04-11 11:37 yakobowski New Issue
2013-04-11 11:37 yakobowski Status new => assigned
2013-04-11 11:37 yakobowski Assigned To => signoles
2013-04-11 13:22 signoles Note Added: 0003787
2013-04-11 13:22 signoles Status assigned => feedback
2013-04-11 13:41 yakobowski Note Added: 0003788
2013-04-11 14:04 signoles Note Added: 0003789
2013-04-11 14:04 signoles Status feedback => acknowledged
2013-04-11 14:04 signoles Note Edited: 0003789
2013-04-20 07:25 signoles Target Version => Frama-C Neon-20140301
2013-06-18 10:47 svn Checkin
2013-06-18 10:47 svn Status acknowledged => resolved
2013-06-18 10:47 svn Resolution open => fixed
2014-02-12 16:58 signoles Note Added: 0004571
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker