--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on June 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Code proved with Fluorine is more proved with Neon



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