--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on July 2015 ---
Hi, Thanks for the report. Option « -wp-unsat-model » has been actually removed, but for the documentation, sorry for the inconvenience. The option « -wp-proof-trace » can be used instead, although it only makes alt-ergo having options « -proof » and « -model » activated, and Why-3 having option « --debug call_prover » ; To get more interesting results with alt-ergo, you can use « -wp-alt-ergo-opt="-complete-model » or any other combination of alt-ergo options. Results are stored on the wp out directory, which you can set with « -wp-out <dir> » ; for instance : (the source code is dummy) run frama-c: $ frama-c -wp foo.i -wp-alt-ergo-opt="-complete-model" -wp-out foo [...] [wp] [Alt-Ergo] Goal typed_foo_post_2 : Unknown (Qed:0.87ms) (234ms) [wp] [Alt-Ergo] Goal typed_foo_post : Unknown (Qed:2ms) (228ms) [...] list output dir: $ find foo [...] foo/typed/foo_post_2_Alt-Ergo.mlw foo/typed/foo_post_2_Alt-Ergo.out foo/typed/foo_post_Alt-Ergo.mlw foo/typed/foo_post_Alt-Ergo.out [...] show proverâs output: $ cat swap/typed/foo_post_Alt-Ergo.out File "swap/typed/foo_post_Alt-Ergo.mlw", line 802, characters 1-781:I don't know. Model Propositional: from_int(0) = 0 from_int(1) = 1 null = {base = 0; offset = 0} hardware(0) = 0 G_z_74 = 75 region(G_z_74) = 0 a = shift_sint32(global(G_z_74),0) x = t_1[a_2] [...] Regards, L. > Le 21 juil. 2015 à 16:42, Daniel Trebbien <dtrebbien at gmail.com> a écrit : > > Hello, > > I am using Frama-C Sodium-20150201. The WP 0.8 plugin manual documents the -wp-unsat-model and -wp-no-unsat-model options on page 22. There is also a thread to this mailing list which mentions the -wp-unsat-model option: > http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-November/004100.html <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-November/004100.html> > > When I try to use -wp-unsat-model, I get an error: > > [kernel] user error: option `-wp-unsat-model' is unknown. > > Also, running frama-c -wp-help does not show the availability of this option. > > Was this feature removed at some point, or was it renamed? > > Daniel Trebbien > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150723/db404b3c/attachment.html>