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



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