Frama-C should not honor -save if when it aborts
ID0001388: This issue was created automatically from Mantis Issue 1388. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001388 | Frama-C | Kernel | public | 2013-04-11 | 2014-03-13 |
| Reporter | yakobowski | Assigned To | signoles | Resolution | fixed |
| Priority | low | Severity | feature | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | Frama-C Neon-20140301 | Fixed in Version | Frama-C Neon-20140301 |
Description :
This is problematic because it complicates the use of Makefile. Typical pattern:
Makefile: foo.sav: $(DEPS) frama-c -save $@
make foo.sav <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?