Command Line Invocation
The following is an overview over the GNATprove commandline options. See also the section Running GNATprove from the Command Line for more detailed information for many of the switches.
Usage: gnatprove -Pproj [switches] [-cargs switches]
proj is a GNAT project file
-cargs switches are passed to gcc
All main units in proj are analyzed by default. Switches to change this:
-u [files] Analyze only the given files
[files] Analyze given files and all dependencies
-U Analyze all files (including unused) of all projects
(can also be used with "--limit-*" switches to analyze
all instances of a generic)
gnatprove basic switches:
-aP=p Add path p to project path
--assumptions Output assumptions information
--clean Remove GNATprove intermediate files, and exit
--cwe Include CWE ids in message output
--explain=Ennnn Output explanation for explain code Ennnn
associated to a message (error, warning or check)
-f Force recompilation/analysis of all units
-h, --help Display this usage information
--info Output info messages about the analysis
-j N Use N parallel processes (default: 1; N=0 will use
all cores of the machine)
-k Do not stop analysis at the first error
--level=n Set the level of proof (0 = faster to 4 = more powerful)
--list-categories Output a list of all message categories and exit
-m Minimal reanalysis
--mode=m Set the mode of GNATprove (m=check, check_all, flow,
prove, all*, stone, bronze, silver, gold)
--no-subprojects Do not analyze subprojects, only the root project
--output-msg-only Do not run any provers, output current flow and proof
results
-q, --quiet Be quiet/terse
--replay Replay proofs, do not attempt new proofs
--report=r Set the report mode of GNATprove (r=fail*, all,
provers, statistics)
--subdirs=p Create all artifacts in this subdir
-v, --verbose Output extra verbose information
--version Output version of the tool and exit
--warnings=w Set the warning mode of GNATprove
(w=off, continue*, error)
-W=warning-tag (warn) Enable the warning corresponding to the tag
-A=warning-tag (allow) Disable the warning corresponding to the tag
-D=warning-tag (deny) Promote the warning corresponding to the tag
to an error
-Xnm=val Specify an external reference for Project Files
* Main mode values
. check - Fast partial check for SPARK violations
. check_all, stone - Full check for SPARK violations
. flow, bronze - Prove correct initialization and data flow
. prove - Prove absence of run-time errors and contracts
. all, silver, gold - Activates all modes (default)
* Report mode values
. fail - Report failures to prove checks (default)
. all - Report all results of proving checks
. provers - Same as all, plus prover usage information
. statistics - Same as provers, plus timing and steps information
* Warning mode values
. off - Do not issue warnings
. continue - Issue warnings and continue (default)
. error - Treat warnings as errors
gnatprove advanced switches:
--check-counterexamples=c
Enable or disable checking of counterexample (c=on*,off)
--checks-as-errors=c Treat unproved check messages as errors (c=on,off*)
--ce-steps=nnn Set the maximum number of proof steps for counterexamples.
This replaces the use of timeout for counterexamples.
--counterexamples=c Enable or disable counterexamples (c=on,off*)
-d, --debug Debug mode
--debug-save-vcs Do not delete intermediate files for provers
--debug-exec-rac Only execute runtime assertion checking (RAC) and exit
--flow-debug Extra debugging for flow analysis (requires graphviz)
--function-sandboxing=c
Enable or disable the generation of guards for axioms
providing contracts of functions (c=on*,off)
--limit-line=f:l Limit analysis to given file and line
--limit-line=f:l:c:k Limit analysis to given file, line, column and kind of
check
--limit-lines=file Limit analysis to lines specified in file (one per line)
--limit-name=s Limit analysis to subprogram with the specified name
--limit-region=f:l:l Limit analysis to given file and range of lines
--limit-subp=f:l Limit analysis to subprogram declared at the specified
location
--memcached-server=host:portnumber
Specify a memcached instance that will be used for
caching of proof results.
--memcached-server=file:directory
Use the fixed string "file" for part before the colon.
The cache will be stored in the directory after the
colon. Best for CI integration.
--memlimit=nnn Set the prover memory limit in MB. Use value 0 for
no limit (default when no level set)
--no-global-generation
Do not generate Global and Initializes contracts from
code, instead assume "null". Note that this option also
implies --no-inlining.
--no-inlining Do not inline calls to local subprograms for proof
--no-loop-unrolling Do not unroll loops with static bounds and no
(in)variant for proof
--output=o Set the output mode of GNATprove (o=brief, oneline,
pretty*)
--output-header Add a header with extra information in the generated
output file
--pedantic Use a strict interpretation of the Ada standard by
enabling the corresponding warnings
--proof-warnings=c Issue warnings by proof (c=on,off*)
--proof-warnings-timeout
Set the timeout for proof warnings
--proof=g[:l] Set the proof modes for generation of formulas
(g=per_check*, per_path, progressive) (l=lazy*, all)
--prover=s[,s]* Use given provers (s=altergo, cvc5*, z3, ..., or s=all
for using all built-in provers)
--RTS=dir Specify the Ada runtime name/location
--steps=nnn Set the maximum number of proof steps (prover-specific)
Use value 0 for no steps limit.
--target=target_name Specify the name of the target platform
--timeout=nnn Set the prover timeout in seconds. Use value 0 for
no timeout (default when no level set)
--why3-conf=f Specify a configuration file for why3
* Output mode values
. brief - Output minimal check message on a single line
. oneline - Output rich check message on a single line
. pretty - Pretty-print check messages for command-line use (default)
* Proof mode values for generation
. per_check - Generate one formula per check (default when no level set)
. per_path - Generate one formula per path for each check
. progressive - Start with one formula per check, then split into
paths when needed
* Proof mode values for laziness
. lazy - Stop at first unproved formula for each check
(most suited for fully automatic proof) (default)
. all - Attempt to prove all formulas
(most suited for combination of automatic and manual proof)
* Prover name values
(Default prover is cvc5.)
. altergo - Use Alt-Ergo
. colibri - Use Colibri
. cvc5 - Use CVC5
. z3 - Use Z3
. ... - Any other prover configured in your .why3.conf file