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
 -f                    Force recompilation/analysis of all units
 -h, --help            Display this usage information
 -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)
 -m                    Minimal reanalysis
     --mode=m          Set the mode of GNATprove (m=check, check_all, flow,
                       prove, all*)
     --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)
 -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     - Full check for SPARK violations
   . flow          - Prove correct initialization and data flow
   . prove         - Prove absence of run-time errors and contracts
   . all           - 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:
 -d, --debug          Debug mode
 --dbg-proof-only     Disable flow analysis (possibly unsound results)
 --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-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.
 --no-axiom-guard     Do not generate guards for axioms defining contracts of
                      functions
 --no-counterexample  Do not generate a counterexample for unproved formulas
 --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
 --output-header      Add a header with extra information in the generated
                      output file
 --pedantic           Use a strict interpretation of the Ada standard
 --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, ...)
 --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.
 --why3-conf=f        Specify a configuration file for why3

 * Proof mode values for generation
   . per_check     - Generate one formula per check (default)
   . 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.)
   (Provers marked with [steps] support the --steps switch.)
   . altergo       - [steps] Use Alt-Ergo
   . cvc4          - [steps] Use CVC4
   . z3            - [steps] Use Z3
   . ...           - Any other prover configured in your .why3.conf file