Command Line InvocationΒΆ
GNATprove is executed with the following command line:
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
gnatprove basic switches:
-aP=p Add path p to project path
--assumptions Output assumptions information
--codepeer=c Enable or disable CodePeer analysis (c=on,off*)
--clean Remove GNATprove intermediate files, and exit
--cwe Include CWE ids in message output
-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)
* 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:
--checks-as-errors Treat unproved check messages as errors
--counterexamples=c Enable or disable counterexamples (c=on,off*)
-d, --debug Debug mode
--debug-save-vcs Do not delete intermediate files for provers
--flow-debug Extra debugging for flow analysis (requires graphviz)
--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-region=f:l:l Limit analysis to given file and range of lines
--limit-subp=s Limit analysis to subprogram defined by file and line
--memcached-server=host:portnumber
Specify a memcached instance that will be used for
caching of proof results.
--memlimit=nnn Set the prover memory limit in MB. Use value 0 for
no limit (default when no level set)
--no-axiom-guard Do not generate guards for axioms defining contracts of
functions
--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
--proof-warnings Issue warnings by proof
--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, cvc4*, 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.
--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 cvc4.)
. altergo - Use Alt-Ergo
. colibri - Use Colibri
. cvc4 - Use CVC4
. z3 - Use Z3
. ... - Any other prover configured in your .why3.conf file