.. _cmdlineoptions: 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 :doc:`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 method ``stainless.collection.List.size``, while ``--functions=size`` will match all methods and functions named ``size``. This option supports ``_`` as wildcard: ``--functions=List._`` will match all ``List`` 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 to ``smt-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=`` Specify in which directory the cache files generated by ``--cache`` and other options should be stored. Defaults to ``.stainless-cache/``. * ``--json=`` 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=`` 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.