Alternative Provers
Installed with SPARK Pro
The provers Alt-Ergo, Colibri, cvc5 and Z3 are installed with the SPARK tool.
By default, GNATprove uses prover cvc5 only. Switch --level
changes the
default to use one or more provers depending on the chosen level (see
Running GNATprove from the Command Line). Switch --prover
allows to
use another prover, or a list of provers. Prover names altergo
,
colibri
, cvc5
and z3
are used to refer to the versions of provers
Alt-Ergo, Colibri, cvc5 and Z3 that are installed with the SPARK toolset. The
string alt-ergo
can also be used to refer to Alt-Ergo. Using the switch
--prover=all
, one can select all four built-in provers, in the order
cvc5, z3, colibri, altergo
. More information on Alt-Ergo, cvc5 and Z3 can
be found on their respective websites:
Alt-Ergo: https://alt-ergo.ocamlpro.com
cvc5: https://cvc5.github.io/
Installed with SPARK Discovery
In this case, only prover Alt-Ergo is installed with the SPARK tool. Hence,
by default GNATprove only uses prover Alt-Ergo. In particular, switch
--level
has no impact on the use of different provers, and --prover=all
will only select Alt-Ergo.
Installed with SPARK Community
The provers Alt-Ergo, cvc5 and Z3 are installed with the SPARK tool.
Other Automatic or Manual Provers
Updating the Why3 Configuration File
GNATprove can call other provers, as long as they are supported by the Why3 platform (see complete list on Why3 webpage). To use another prover, it must be listed in your Why3 configuration file.
To create or update automatically a Why3 configuration file, call the command
<spark2014-install>/libexec/spark/bin/why3config --detect-provers
. It
searches your PATH
for any supported provers and adds them to the default
configuration file .why3.conf
in your HOME
, or a configuration file
given in argument with switch -C <file>
. This file consists of a few
general settings and a section for each prover which is supported.
Note that GNATprove never reads the default configuration file .why3.conf
in your HOME
. You need to pass the configuration file explicitly with
switch --why3-conf=<file>
. Any prover name configured in this configuration
file can be used as an argument to switch --prover
.
Note that using this mechanism, you cannot replace the definitions provided
with the SPARK tools for the provers altergo
, colibri
, cvc5
and
z3
.
If more than one prover is specified, the provers are tried in order on each VC, until one of them succeeds or all fail. Interactive provers cannot be combined with other provers, so must appear on their own.
Coq
gnatprove
has support for the Coq interactive prover, even though Coq is
not part of the SPARK distribution. If you want to use Coq with SPARK, you
need to install it yourself on your system and put it in your PATH
environment variable. Then, you can simply provide --prover=coq
to
gnatprove
. Note that the only supported version currently is Coq 8.11.