--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on June 2014 ---
I had a look to this issue yesterday and tried to understand this difference. As lo?c said, this is due to case-split analysis issue over huge integer intervals. Alt-Ergo either timeouts (with option -max-split -1) or answers "I don't know" (with the default value of option -max-split). The shape of VCs generated by Neon may be different from those of Fluorine (they may contain more integer intervals). This could explain the behavior of Alt-Ergo. I implemented a small fix and this seems to work better: *for f in add_times_*.mlw do ** ** timeout 60 ./alt-ergo.opt -max-split -1 $f** **done* File "add_times_assign_part1_Alt-Ergo.mlw", line 770, characters 1-1119:Valid (0.0485) (57) File "add_times_assign_part2_Alt-Ergo.mlw", line 770, characters 1-1119:Valid (0.0504) (57) File "add_times_assign_part3_Alt-Ergo.mlw", line 770, characters 1-1274:Valid (0.0904) (63) File "add_times_assign_part4_Alt-Ergo.mlw", line 770, characters 1-1274:Valid (0.0907) (63) File "add_times_complete_nsec_sum_less_than_1s_nsec_sum_higher_____Alt-Ergo.mlw", line 770, characters 1-1169:Valid (0.0343) (33) File "add_times_disjoint_nsec_sum_less_than_1s_nsec_sum_higher_____Alt-Ergo.mlw", line 770, characters 1-1169:Valid (0.0345) (33) File "add_times_nsec_sum_higher_than_1s_post_2_Alt-Ergo.mlw", line 770, characters 1-1806:Valid (17.9307) (240) File "add_times_nsec_sum_higher_than_1s_post_3_Alt-Ergo.mlw", line 770, characters 1-1734:Valid (13.4213) (169) File "add_times_nsec_sum_higher_than_1s_post_Alt-Ergo.mlw", line 770, characters 1-1793:Valid (42.8524) (250) File "add_times_nsec_sum_less_than_1s_post_2_Alt-Ergo.mlw", line 770, characters 1-1788:Valid (25.4911) (240) File "add_times_nsec_sum_less_than_1s_post_3_Alt-Ergo.mlw", line 770, characters 1-1731:Valid (11.3075) (169) File "add_times_nsec_sum_less_than_1s_post_Alt-Ergo.mlw", line 770, characters 1-1786:Valid (33.3877) (250) - Mohamed. -- Senior R&D Engineer, OCamlPro Research Associate, VALS team, LRI. http://www.iguer.info Le 02/06/2014 11:11, Lo?c Correnson a ?crit : > 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 > _______________________________________________ > 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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140602/79285296/attachment-0001.html>