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