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] Jessie and why3

  • Subject: [Frama-c-discuss] Jessie and why3
  • From: Claude.Marche at inria.fr (Claude Marché)
  • Date: Mon, 25 Aug 2014 10:55:00 +0200
  • In-reply-to: <1406816696.63286.YahooMailNeo@web140905.mail.bf1.yahoo.com>
  • References: <1406816696.63286.YahooMailNeo@web140905.mail.bf1.yahoo.com>
= short answer =

you should do

frama-c -jessie mean.c

and run Z3 on all goals using the GUI. It is advised to split the goals
in parts using "Split" if running Z3 on a whole VC does not work.

= longer answer =

There is no (easy) way to run a given prover on each VC generated by
Jessie/Why3. The reason is that Why3 should not be used using a single
prover like this. By running the Why3 GUI, the user should interact with
the goals, splitting them, try various provers, change the time limit
for some goals, inline some symbols, and generally speaking apply
transformations. The session mechanism of Why3 is there to memoize all
these tasks and replay them easily when modifying the output program.

hope this helps,

- Claude


Le 31/07/2014 16:24, Artem Kalinovsky a ?crit :
> Hi!
> 
> I want run Jessie with Z3 and Why3
> 
> Now my command looks like this:
> frama-c -jessie -jessie-atp z3 mean.c.
> 
> I checked out that -jessie-atp calls Why2. How can I call why3 instead
> of why3?
> 
> I was trying to find answer in "jessie tutorial" but there was no
> solution for my issue.
> 
> Thank you!
> 
> 
> 
> _______________________________________________
> 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
> 

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |