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

Hi David,

This is not a bug. By default, warning are not stored in the save
file. However, the option -collect-messages is what you are looking
for.

(We are trying to transition to a state where all alarms emitted by
Value are stored as ACSL properties, so that the 'messages' panel will
ultimately be fully redundant. We're not there yet, though.)

On Mon, Sep 1, 2014 at 6:04 PM, David MENTRE <dmentre at linux-france.org> wrote:
>
> 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
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss



-- 
Boris