--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on April 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] which provers to use



You should do

   why3config --detect

before using why3ide

- Claude

Le 09/04/2013 17:56, Stephen Siegel a ?crit :
> Hi all, I have Frama-C working with the Jessie plugin (thanks for help everyone), but the only prover I have managed to get working is CVC3.  I have read some of the Why web pages but am a little confused about what is supported.  I've installed why2 and why3, and the latest Alt-Ergo, Z3, cvc3, and Gappa.
>
> Here's my report from why2-config:
>
>      prover      version              info   invocation
> ------------------------------------------------------
>    Alt-Ergo       0.95.1   (not supported)   alt-ergo
>    Simplify                      not found
>     Vampire                      not found
>          Z3        4.3.2   (not supported)   z3 -smt
>       Yices                      not found
>        CVC3        2.4.1                     cvc3 -lang smt
>        CVCL        2.4.1                     cvc3
>       Gappa       0.17.1   (not supported)   gappa
>         Coq                      not found
>         PVS                      not found
>       VeriT                      not found
>       Zenon                      not found
> ------------------------------------------------------
>
> When I run frama-c -jessie, the why3ide shows only CVC3.  Should I be looking for older versions of some of these provers that are compatible with why?
>
>
> _______________________________________________
> 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                    |