2021-03-01 05:52 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000635Frama-CKernelpublic2014-02-12 16:55
Assigned Tosignoles 
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 Files
  • c file icon test.c (102 bytes) 2010-12-13 10:55 -
    volatile int V1;
    int tab[10];
    int main(void)
      int l = V1;
      tab[l] = 1;
      return tab[V1];
    c file icon test.c (102 bytes) 2010-12-13 10:55 +




signoles (manager)

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)

Last edited: 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)

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)

I undestand now, ok for a feature (an intersting feature).


signoles (manager)

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
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
2013-12-19 01:12 signoles Source_changeset_attached => framac master 291e8f7a
2014-02-12 16:55 signoles Source_changeset_attached => framac stable/neon 291e8f7a
+Issue History