Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Issue with -save/-load options, warning not displayed in GUI

  • Subject: [Frama-c-discuss] Issue with -save/-load options, warning not displayed in GUI
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Mon, 01 Sep 2014 18:04:26 +0200
Hello,

I'm using latest Frama-C (from opam):
"""
$ frama-c --version
Version: Neon-20140301
"""

I use following warn.c program:
"""
int main(int x)
{
   int a = x / 0;

   return a;
}
"""

If I launch the GUI using "frama-c-gui -val warn.c", I do have an assert 
in the displayed code and a warning in the Messages panel. So far so good.

Now, I first do an analysis and then I load the result in the GUI:
   frama-c -val warn.c -save warn.saved

   frama-c-gui -load warn.saved

In that case, I still have an assert in the displayed code but the 
warning is no longer displayed in the Messages panel. I think it should be.

As far as I remember, it was a feature of a previous versions of Frama-C 
(I haven't checked). It works as I expected (warning displayed in 
Messages panel) in TrustInSoft's proprietary version of Frama-C.

Thus my questions:
1. Is this a bug or a feature of Frama-C Neon? Do I miss-use Frama-C? 
Our use of -save/-load is to do some lengthy analysis first and then 
display the GUI very quickly several times.

2. If this a bug, should I open a bug report?

3. Is there a work around?

Best regards,
david