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] adding new provers to why3

Subject: [Frama-c-discuss] adding new provers to why3
From: Claude.Marche at inria.fr (Claude Marche)
Date: Tue, 12 Nov 2013 01:28:57 +0100
In-reply-to: <BAY169-W40E168A61B828C685AA5F097FF0@phx.gbl>
References: <BAY169-W100232DF1943ABFB9A9A5BF97F20@phx.gbl>, <CAC3Lx=ZroHdwUmVz1riwHgC+Y0LD0CabO0LyQrJ_UJD9837sWg@mail.gmail.com> <BAY169-W40E168A61B828C685AA5F097FF0@phx.gbl>


As suggested by Virgile, Why3 cannot find the Simplify executable if its
names finished with .linux or .macos or whatever.

The possible names of provers' executables are not easy to guess. For
those who want to know, Why3 looks for the names that are listed in the
file

/usr/local/share/why3/provers-detection-data.conf

- Claude

References:
- [Frama-c-discuss] adding new provers to why3
  - From: x_cui at hotmail.com (Xiao-lei Cui)
- [Frama-c-discuss] adding new provers to why3
  - From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] adding new provers to why3
  - From: x_cui at hotmail.com (Xiao-lei Cui)

Prev by Date: [Frama-c-discuss] adding new provers to why3
Next by Date: [Frama-c-discuss] Why wp plugin failed to prove such naive properties?
Previous by thread: [Frama-c-discuss] adding new provers to why3
Next by thread: [Frama-c-discuss] math vs. bits
Index(es):
- Date
- Thread