--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on June 2012 ---
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