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?

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