--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on December 2014 ---
You shall use option '-wp-gen? to generate the proof obligations without sending them to the prover. 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. Regards, L. Le 15 d?c. 2014 ? 09:13, David MENTRE <dmentre at linux-france.org> a ?crit : > Hello, > > Le 15/12/2014 08:55, David MENTRE a ?crit : >> You should use -wp-qed-checks but it seems to be broken in WP 0.8 >> (generation of truncated Alt-Ergo files). > > Submitted as BTS bug 2031: > https://bts.frama-c.com/view.php?id=2031 > > BTW, on frama-c.com website, URL http://bts.frama-c.com (used in http://frama-c.com/support.html page) does not work. Only its HTTPS version does. > > 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