2021-01-26 19:55 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000635Frama-CKernelpublic2010-12-09 10:322014-02-12 16:55
Reportersduprat 
Assigned Tosignoles 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
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 +

-Relationships
+Relationships

-Notes

~0001303

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?

~0001307

sduprat (reporter)

2010-12-13 10:53

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.

~0001308

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".

~0001309

sduprat (reporter)

2010-12-13 12:22

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

~0001347

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
+Notes

-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