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