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



Probably one more instance of Alt-Ergo case splitting strategy, which is obfuscated by the large constants introduced by int32 / int64 boundaries. This is a known issue with Alt-Ergo.

The -wp-split option explicitly introduces more case splits before sending proof obligations to the provers.
	L.


Le 2 juin 2014 ? 08:53, David MENTRE <dmentre at linux-france.org> a ?crit :

> 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
> 
> _______________________________________________
> 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