--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on December 2014 ---
Hello Lo?c, Le 15/12/2014 09:40, Lo?c Correnson a ?crit : > You shall use option '-wp-gen? to generate the proof obligations without sending them to the prover. But this does not generate anything for simple VCs! For example: """ $ cat f_wp.c /*@ requires 0 <= x <= 10; ensures 1 <= \result <= 11; */ int f(int x) { return x + 1; } """ $ frama-c -wp-out out -wp -wp-gen f_wp.c [kernel] preprocessing with "gcc -C -E -I. f_wp.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] 1 goal scheduled [wp] [Qed] Goal typed_f_post : Valid [wp] Proved goals: 1 / 1 Qed: 1 $ ls out ls: cannot access out: No such file or directory """ Would you have a command line that works on above program? Above command line works with more complicated program, like: """ *@ requires 0 <= x <= 10; ensures 0 <= \result <= 33; */ int f_complicated(int x) { return x * 3; } """ > The ? *.ergo ? files only contains the goal part, without the necessary libraries and definitions, which are generated aside. > The ? *_Alt-Ergo.mlw ? files are self-contained. I understand that *.ergo files contain only goals. But a goal like "goal Qed_19_20: (0 <" seems rather strange to me. Best regards, david