--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on June 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] alt-ergo silently ignored / any idea?



Hi,

investigating further, I found something.

Running:
$ TEMP=/c/Temp frama-c -wp  -wp-rte -wp-trace -wp-proof alt-ergo  /c/src/wp.c

the following files were created in

$ ls /c/Temp/wp10f3bb.dir/
store_swap_assert_1_rte_ergo.txt  store_swap_assert_4_rte_ergo.txt
store_swap_assert_2_rte_ergo.txt  store_swap_post_1_A_ergo.txt
store_swap_assert_3_rte_ergo.txt  store_swap_post_2_B_ergo.txt

but there are all empty. Is this what is expected?

Thanks,
Sylvain

On Tue, Jun 19, 2012 at 5:14 PM, Virgile Prevosto
<virgile.prevosto at m4x.org> wrote:
> Hello Sylvain,
>
> 2012/6/19 sylvain nahas <sylvain.nahas at googlemail.com>:
>> I am trying to get Nitrogen to work with alt-ergo on MS Windows XP.
>> Building seems going OK, but when calling wp on the sample source file
>> from the manual, I can not get an output that indicates that alt-ergo
>> is actually called.
>> It seems silently ignored.
>>
>> alt-ergo ist accessible in PATH and working correctly, as far as I can judge.
>> Its version is 0.94.
>>
>> Sample output :
>> -------------------------------------------------------------------------
>> $ frama-c -wp ?-wp-proof alt-ergo ?/c/src/wp.c
>> [kernel] preprocessing with "gcc -C -E -I. ?c:/src/wp.c"
>> [wp] warning: Missing RTE guards
>> [wp] [WP:simplified] Goal store_swap_function_assigns : Valid
>> -------------------------------------------------------------------------
>> Notice that there is no mention of alt-ergo!
>
> It's merely because WP was smart enough to detect itself that the
> assigns clause is valid: there is a small simplifier before provers
> are called, and if it is able to reduce a PO to \true, no prover is
> called. You'll have to provide more complicated annotations to test
> the call to alt-ergo ;-)
>
> Best regards,
> --
> E tutto per oggi, a la prossima volta
> Virgile
>
> _______________________________________________
> 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