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

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