Command Line Options¶
Stainless’s command line options have the form
To enable a flag option, use
--option. To disable a flag option, use
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
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
Choosing which Stainless feature to use¶
The first group of options determines which feature of Stainless will be used.
--verification is chosen.
Proves or disproves function contracts, as explained in the Verification conditions section.
Evaluate parameterless functions and report their body’s value and whether or not their postcondition holds.
Prints a helpful message, then exits.
Additional top-level options¶
These options are available to all Stainless components:
Re-run the selected analysis components upon file changes, making the program analysis interactive and significantly more efficient than restarting stainless manually.
Reduces the components’ summaries to only the invalid elements (e.g. invalid VC).
--infer-measures=[yes|no|only] (default: yes)
Infers measures for recursive functions which do not already have one.
--check-measures=[true|false] (default: true)
Check termination of functions with measures, ie. whether measures decrease between recursive calls.
Enables printing detailed messages for the components d1,d2,… . Available components are:
solver(SMT solvers and their wrappers)
timers(Timers, timer pools)
trees(Manipulation of trees)
full-vc(Display VCs before and after simplification)
type-checker(Type checking of the final program for VC generation)
type-checker-vcs(Generation of VCs by the type-checker)
derivation(Dump typing derivations)
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.sizewill match the method
--functions=sizewill match all methods and functions named
size. This option supports
--functions=List._will match all
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
nativez3solver 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:
Native Z3 with z3-templates for unfolding recursive functions (default).
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
cvc4executable in your system path (the latest unstable version is recommended).
Z3 through SMT-LIB. To use this or the next solver, you need to have the
z3executable in your program path (the latest stable version is recommended). Inductive reasoning happens on the Stainless side (similarly to
Native Z3, but inductive reasoning happens within Stainless (similarly to
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.
Set a timeout for each attempt to prove one verification condition/ repair one function (in sec.) When using the
--evalcomponent, one should use
Use persistent cache on disk to save the state of the verification and/or termination analyses.
Specify in which directory the cache files generated by
--cacheand other options should be stored. Defaults to
Export the verification and/or termination analyses to the given file.
Fetch the specified dependencies, and add their sources to the set of files processed by Stainless. Each dependency must be available as a source JAR from MavenCentral, the EPFL-LARA bintray organization, your local Ivy database, or through another resolver specified via
Note: Stainless will not pull transitive dependencies, so one has to specify all transitive dependencies explicitely via this option.
Specify additional resolvers to be used to fetch the dependencies specified via the
Note: The full URL of the resolver must be used.
See the Coursier source code for the list of most common repositories URLs.
Additional Options (by component)¶
The following options relate to specific components in Stainless.
Check arithmetic operations for unintended behaviour and overflows.
Use a persistent cache mechanism to speed up verification; on by default.
Aborts verification as soon as a VC cannot be proven to be correct.
Aborts verification as soon as an invalid VC is found.
Ignore postconditions during termination verification.
Double-check counterexamples with the evaluator.
Use evaluator to find counterexamples early.
Use unsat-assumptions to drive unrolling while remaining fair.
Don’t crash on errors, simply return
Speeds up unrolling by a factor
Boosts model-finding capabilities by a factor
n. This may come at the cost of proof construction.
Disables program simplification heuristics.
Pass extra command-line arguments to CVC4.
Use compiled evaluator instead of an interpreter.
Assume all arrays can fit into memory during compiled evaluation.
Instrument ADT field access during code generation.
Bounds the total number of function call evaluations (before crashing).
Ignores function contracts during evaluation.
Stainless supports setting default values for command line options configuration files.
The file must be named
.stainless.conf and be a valid HOCON file.
For example, consider the config file containin the following lines:
vc-cache = false debug = [verification, trees] timeout = 5 check-models = true print-ids = true
The file will translate to the following command line options:
--vc-cache=false --debug=verification,trees --timeout=5 --print-ids
Stainless searches for a configuration file recursively
starting from the current directory and walking up the
directory hierarchy. For example, if one runs stainless
/a/b/c and there is a config file in any of c,
b or a, the first of those is going to be loaded.