Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] [wp] Was -wp-unsat-model removed?
  • From: loic.correnson at cea.fr (Loïc Correnson)
  • Date: Thu, 23 Jul 2015 10:15:12 +0200
  • In-reply-to: <CABrgu5TJqnW-Pvcfi2oQoC+WpVbju-pqXURx1nT=MPdoatc1XQ@mail.gmail.com>
  • References: <CABrgu5TJqnW-Pvcfi2oQoC+WpVbju-pqXURx1nT=MPdoatc1XQ@mail.gmail.com>
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>