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



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>