--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on December 2014 ---
OK. Goals named after ? Qed_nnn ? are auto-checks generated by WP on-the-fly for asserting the soundness of Qed simplifications. This was a very experimental feature that shall not survive to the next release of Frama-C ;-) Sorry for my misunderstanding. L. Le 15 d?c. 2014 ? 09:57, David MENTRE <dmentre at linux-france.org> a ?crit : > 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 > > _______________________________________________ > 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