--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on September 2014 ---
[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



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