--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on July 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [wp] Was -wp-unsat-model removed?



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>