Frama-C Bug Tracking System - Frama-C
View Issue Details
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.
Relationships
Attached Files

Notes
(0003787)
signoles   
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   
2013-04-11 13:41   
Great idea. This is much neater, and will indeed not cause problems with debugging.
(0003789)
signoles   
2013-04-11 14:04   
Will be implemented. Hopefully it is not Fluorine-critical...
(0004571)
signoles   
2014-02-12 16:58   
Fix committed to stable/neon branch.

Issue History
Date ModifiedUsernameFieldChange
2013-04-11 11:37yakobowskiNew Issue
2013-04-11 11:37yakobowskiStatusnew => assigned
2013-04-11 11:37yakobowskiAssigned To => signoles
2013-04-11 13:22signolesNote Added: 0003787
2013-04-11 13:22signolesStatusassigned => feedback
2013-04-11 13:41yakobowskiNote Added: 0003788
2013-04-11 14:04signolesNote Added: 0003789
2013-04-11 14:04signolesStatusfeedback => acknowledged
2013-04-11 14:04signolesNote Edited: 0003789
2013-04-20 07:25signolesTarget Version => Frama-C Neon-20140301
2013-06-18 10:47svn
2013-06-18 10:47svnStatusacknowledged => resolved
2013-06-18 10:47svnResolutionopen => fixed
2013-12-19 01:11signolesSource_changeset_attached => framac master a4e797cc
2014-02-12 16:53signolesSource_changeset_attached => framac stable/neon a4e797cc
2014-02-12 16:58signolesNote Added: 0004571
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed