| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001388 | Frama-C | Kernel | public | 2013-04-11 11:37 | 2014-03-13 15:57 | ||||
| Reporter | yakobowski | ||||||||
| Assigned To | signoles | ||||||||
| Priority | low | Severity | feature | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | |||||||||
| Target Version | Frama-C Neon-20140301 | Fixed in Version | Frama-C Neon-20140301 | ||||||
| Summary | 0001388: Frama-C should not honor -save if when it aborts | ||||||||
| Description | This 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? | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
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? |
|
yakobowski (manager) 2013-04-11 13:41 |
Great idea. This is much neater, and will indeed not cause problems with debugging. |
|
signoles (manager) 2013-04-11 14:04 Last edited: 2013-04-11 14:04 |
Will be implemented. Hopefully it is not Fluorine-critical... |
|
signoles (manager) 2014-02-12 16:58 |
Fix committed to stable/neon branch. |
| Notes |
| 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 | ||
| 2013-06-18 10:47 | svn | Status | acknowledged => resolved |
| 2013-06-18 10:47 | svn | Resolution | open => fixed |
| 2013-12-19 01:11 | signoles | Source_changeset_attached | => framac master a4e797cc |
| 2014-02-12 16:53 | signoles | Source_changeset_attached | => framac stable/neon a4e797cc |
| 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 |
| Issue History |