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] alt-ergo silently ignored / any idea?

  • Subject: [Frama-c-discuss] alt-ergo silently ignored / any idea?
  • From: sylvain.nahas at googlemail.com (sylvain nahas)
  • Date: Tue, 19 Jun 2012 18:18:33 +0200
  • In-reply-to: <CA+yPOVhMFXw3r9y_vh_YcgJ-TCL3H1yuYT_==OGjaEdy69ny5A@mail.gmail.com>
  • References: <CAFaEDLC0QHAoOfUC6mE9fGL8da4JPBC_JoHM2zCBH-9iQ+UnBA@mail.gmail.com> <CA+yPOVhMFXw3r9y_vh_YcgJ-TCL3H1yuYT_==OGjaEdy69ny5A@mail.gmail.com>
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