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

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>