0001388: Frama-C should not honor -save if when it aborts - Frama-C Bug Tracking System

Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ 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

Platform

OS

OS Version

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 -save $@ make foo.sav 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.

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 - 2019 MantisBT Team