Command Line Options¶
Stainless’s command line options have the form --option
or --option=value
.
To enable a flag option, use --option=true
or on
or yes
,
or just --option
. To disable a flag option, use --option=false
or off
or no
.
Additionally, if you need to pass options to the scalac
frontend of Stainless,
you can do it by using a single dash -
. For example, try -Ybrowse:typer
.
The rest of this section presents command-line options that Stainless recognizes.
For a short (but always up-to-date) summary, you can also invoke stainless --help
.
Choosing which Stainless feature to use¶
The first group of options determines which feature of Stainless will be used.
By default, --verification
is chosen.
--verification
Proves or disproves function contracts, as explained in the Verification section.
--termination
Runs termination analysis. Can be used along
--verification
.--eval
Evaluate parameterless functions and report their body’s value and whether or not their postcondition holds.
--help
Prints a helpful message, then exits.
Additional top-level options¶
These options are available to all Stainless components:
--watch
Re-run the selected analysis components upon file changes, making the program analysis interactive and significantly more efficient than restarting stainless manually.
--compact
Reduces the components’ summaries to only the invalid elements (e.g. invalid VC).
--debug=d1,d2,...
Enables printing detailed messages for the components d1,d2,… . Available components are:
solver
(SMT solvers and their wrappers)termination
(Termination analysis)timers
(Timers, timer pools)trees
(Manipulation of trees)verification
(Verification)
--functions=f1,f2,...
Only consider functions f1, f2, … . This applies to all functionalities where Stainless manipulates the input in a per-function basis.
Stainless will match against suffixes of qualified names. For instance:
--functions=List.size
will match the methodstainless.collection.List.size
, while--functions=size
will match all methods and functions namedsize
. This option supports_
as wildcard:--functions=List._
will match allList
methods.--solvers=s1,s2,...
Use solvers s1, s2,… . If more than one solver is chosen, all chosen solvers will be used in parallel, and the best result will be presented. By default, the
nativez3
solver is picked.Some solvers are specialized in proving verification conditions and will have a hard time finding a counterexample in the case of an invalid verification condition, whereas some are specialized in finding counterexamples, and some provide a compromise between the two. Also, some solvers do not as of now support higher-order functions.
Available solvers include:
nativez3
Native Z3 with z3-templates for unfolding recursive functions (default).
smt-cvc4
CVC4 through SMT-LIB. An algorithm within Stainless takes up the unfolding of recursive functions, handling of lambdas etc. To use this or any of the following CVC4-based solvers, you need to have the
cvc4
executable in your system path (the latest unstable version is recommended).smt-z3
Z3 through SMT-LIB. To use this or the next solver, you need to have the
z3
executable in your program path (the latest stable version is recommended). Inductive reasoning happens on the Stainless side (similarly tosmt-cvc4
).unrollz3
Native Z3, but inductive reasoning happens within Stainless (similarly to
smt-z3
).princess
Princess solver through its native interface (uses princess-templates) during unfolding. This is a full-stack JVM solver and enables Stainless to run without external solver dependencies.
--timeout=t
Set a timeout for each attempt to prove one verification condition/ repair one function (in sec.) When using the
--eval
component, one should use--max-calls
instead.--cache
Use persistent cache on disk to save the state of the verification and/or termination analyses.
--cache-dir=<directory>
Specify in which directory the cache files generated by
--cache
and other options should be stored. Defaults to.stainless-cache/
.--json=<file>
Export the verification and/or termination analyses to the given file.
Additional Options (by component)¶
The following options relate to specific components in Stainless.
Verification¶
--strict-aritmetic
Check arithmetic operations for unintended behaviour and overflows.
--vc-cache
Use a persistent cache mechanism to speed up verification; on by default.
--fail-early
Aborts verification as soon as a VC cannot be proven to be correct.
--fail-invalid
Aborts verification as soon as an invalid VC is found.
Termination¶
--ignore-posts
Ignore postconditions during termination verification.
Unrolling Solver¶
--check-models
Double-check counterexamples with the evaluator.
--feeling-lucky
Use evaluator to find counterexamples early.
--unroll-assumptions
Use unsat-assumptions to drive unrolling while remaining fair.
--silent-errors
Don’t crash on errors, simply return
Unknown
.--unroll-factor=n
Speeds up unrolling by a factor
n
.--model-finding=n
Boosts model-finding capabilities by a factor
n
. This may come at the cost of proof construction.--no-simplifications
Disables program simplification heuristics.
CVC4 Solver¶
--solver:cvc4=<cvc4-opt>
Pass extra command-line arguments to CVC4.
Evaluators¶
--codegen
Use compiled evaluator instead of an interpreter.
--small-arrays
Assume all arrays can fit into memory during compiled evaluation.
--instrument
Instrument ADT field access during code generation.
--max-calls=n
Bounds the total number of function call evaluations (before crashing).
--ignore-contracts
Ignores function contracts during evaluation.