Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000635Frama-CKernelpublic2010-12-09 10:322014-02-12 16:55
Assigned Tosignoles 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20110201 
Summary0000635: losing messages doing save/load
DescriptionThe option "-save" is efficient to save state of the projet, for example, values computed by the value analysis. We are able to retrieve these values in an other session with the "-load" option. But it seems that warnings previously displayed in "message" tab are lost in the opened project.
TagsNo tags attached.
Attached Filesc file icon test.c [^] (102 bytes) 2010-12-13 10:55 [Show Content]

- Relationships

-  Notes
signoles (manager)
2010-12-09 16:40

I tried to reproduce your issue on a single example but it works as expected: the "message" tab contains the same message after -load than before -save. Please could you give us an example with all the necessary infos in order to be able to reproduce your issue?
sduprat (reporter)
2010-12-13 10:53
edited on: 2010-12-13 10:55

On my small example, it works fine when i save the session throw the gui, but it does not work with the following batch command : frama-c -val test.c -save test1.session frama-c-gui -load test1.session the exemple c file is in attachment.
signoles (manager)
2010-12-13 10:59

OK. I understand your issue now. When you execute Frama-C via the batch command, the messages are not stored by Frama-C (thus not saved and then not reloaded). That's a feature, not a bug :). Thus I classify your issue as a "feature request".
sduprat (reporter)
2010-12-13 12:22

I undestand now, ok for a feature (an intersting feature).
signoles (manager)
2010-12-21 17:40

This feature is now implemented. You have to use the new option -collect-messages like this: $ frama-c -collect-messages -val test.c -save test1.session $ frama-c-gui -load test1.session

- Issue History
Date Modified Username Field Change
2010-12-09 10:32 sduprat New Issue
2010-12-09 16:40 signoles Note Added: 0001303
2010-12-09 16:40 signoles Assigned To => signoles
2010-12-09 16:40 signoles Status new => feedback
2010-12-13 10:53 sduprat Note Added: 0001307
2010-12-13 10:55 sduprat File Added: test.c
2010-12-13 10:55 sduprat Note Edited: 0001307
2010-12-13 10:59 signoles Note Added: 0001308
2010-12-13 10:59 signoles Severity minor => feature
2010-12-13 10:59 signoles Status feedback => acknowledged
2010-12-13 12:22 sduprat Note Added: 0001309
2010-12-21 17:39 svn Checkin
2010-12-21 17:39 svn Status acknowledged => resolved
2010-12-21 17:39 svn Resolution open => fixed
2010-12-21 17:40 signoles Note Added: 0001347
2011-02-09 14:36 signoles Status resolved => closed
2011-02-09 14:37 signoles Fixed in Version => Frama-C Carbon-20110201

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker