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