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

---

• Subject: [Frama-c-discuss] which provers to use
• From: Claude.Marche at inria.fr (Claude Marché)
• Date: Tue, 09 Apr 2013 18:04:27 +0200
• In-reply-to: <500749DB-ED6B-4CCD-8C3A-CA4A505C4D6E@udel.edu>
• References: <CAOH62JgFFuwTA_cQpPALG4wHx8-bmWGjPHN7+eji73Yooovqaw@mail.gmail.com> <CAOH62Jg8KeGbqL_L6-Co2RofRvT+KqkcTgTWv2yuzC7pE8aCQQ@mail.gmail.com> <887A9EEF-2A1A-4EDA-BCCD-3C3CBB16E74D@udel.edu> <5162DEA7.5000504@inria.fr> <2B730EC4-CE90-4D06-91BA-BE4794D8D6FD@cea.fr> <500749DB-ED6B-4CCD-8C3A-CA4A505C4D6E@udel.edu>

---

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                    |

---

• Follow-Ups:
  • [Frama-c-discuss] which provers to use
    • From: siegel at udel.edu (Stephen Siegel)

• References:
  • [Frama-c-discuss] installing frama-c on Mac
    • From: siegel at udel.edu (Stephen Siegel)
  • [Frama-c-discuss] installing frama-c on Mac
    • From: Claude.Marche at inria.fr (Claude Marché)
  • [Frama-c-discuss] installing frama-c on Mac
    • From: loic.correnson at cea.fr (Loïc Correnson)
  • [Frama-c-discuss] which provers to use
    • From: siegel at udel.edu (Stephen Siegel)

• Prev by Date: [Frama-c-discuss] installing Jessie plug-in
• Next by Date: [Frama-c-discuss] which provers to use
• Previous by thread: [Frama-c-discuss] which provers to use
• Next by thread: [Frama-c-discuss] which provers to use
• Index(es):
  • Date
  • Thread