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] Code proved with Fluorine is more proved with Neon

  • Subject: [Frama-c-discuss] Code proved with Fluorine is more proved with Neon
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Mon, 02 Jun 2014 08:53:24 +0200
  • In-reply-to: <87mwe3sjnb.fsf@suntof.isae.fr>
  • References: <87mwe3sjnb.fsf@suntof.isae.fr>
Hello,

Le 27/05/2014 10:36, Christophe Garion a ?crit :
> I have some code that was proved with the Fluorine version of Frama-C
> and is no more proved using Neon. A simplified version of the code is
> available in the test_po_time_double_behavior_1.c file.

Everything is proved with -wp-split. Don't ask me why :-) (even if I 
think you are on the border line of what Alt-Ergo can prove).

Command line used:
  frama-c-gui -pp-annot -wp-timeout 60  -wp -wp-split 
test_po_time_double_behavior_1.c


Best regards,
david