[Why3-club] why3 via command line

Maria Christofi maria.christofis at gmail.com
Tue Nov 26 15:12:56 CET 2013


I used to use frama-c with why and I am now turning on why3.

I have a question about its use via the command line.

I m searching somehing similar to "frama-c -jessie -jessie-atp
<prover>" in such a way that it can be read inside the session.
I am explaining what I mean:
I want to run jessie in a c file with a specific prover (or every
possible prover) using a command line (and not the gui) and be able to
see the results in the report produced by .mlw.

If I run just "frama-c -jessie -jessie-atp <prover>" (as with why
before) I cant see the results in the report.

I dont know if my question is clear enough...

Thanks in advance!

Maria Christofi

More information about the Why3-club mailing list