--- layout: fc_discuss_archives title: Message 6 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



David MENTRE <dmentre at linux-france.org> writes:

> 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

Thanks, I have forgotten to try to split the assertions, it works
perfectly now.

Best regards,

Christophe

-- 
Christophe Garion          ISAE/DMIA - SUPAERO/IN
garion at isae.fr             10 avenue Edouard Belin
T?l : (33)5 61 33 80 57    BP 54032
Fax : (33)5 61 33 83 45    31055 Toulouse Cedex 4