--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on December 2014 ---
Hello, Le 15/12/2014 05:17, Debasmita Lohar a ?crit : > The exact commands and outputs are as follows: > 1. frama-c -wp-print test.c. Output: [kernel] preprocessing with "gcc -C > -E -I. test.c" > 2. frama-c -wp-out wptest test.c. Output: same. wptest is a directory > and after the execution of this command it contains nothing. > 3. frama-c -wp-gen test.c. Output: again same. > 4. frama-c -wp test.c. > output: [kernel] preprocessing with "gcc -C -E -I. test.c" > [wp] Running WP plugin... > [wp] Collecting axiomatic usage > [wp] warning: Missing RTE guards > [wp] 1 goal scheduled > [wp] [Qed] Goal typed_main_assert_P : Valid OK, you have several issues: 1. You should use *simultaneously* -wp (to generate and prove proof obligations) and -wp-out <dir> (to keep them in the given <dir> directory) options; 2. Your program is too simple and the generated proof obligation is prove by Qed (line "[Qed] Goal typed_main_assert_P : Valid"), the internal prover of WP, and not Alt-Ergo (thus no file are generated). You should use -wp-qed-checks but it seems to be broken in WP 0.8 (generation of truncated Alt-Ergo files). For 2., another option is to use more complicated proof obligations. For example, on the attached simple_wp.c file, verification condition of f_complicated() is generated (and not for f()). I used following command line: frama-c -wp-out simple_wp_out -wp simple_wp.c Best regards, david -------------- next part -------------- /*@ requires 0 <= x <= 10; ensures 1 <= \result <= 11; */ int f(int x) { return x + 1; } /*@ requires 0 <= x <= 10; ensures 0 <= \result <= 33; */ int f_complicated(int x) { return x * 1; }