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] which provers to use

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?