Repository navigation
Adding a section about command line arguments - #33
Open
marcoeilers wants to merge 1 commit into
Open
marcoeilers wants to merge 1 commit into
marcoeilers wants to merge 1 commit into
Conversation
Aurel300
reviewed
Oct 12, 2026
| @@ -0,0 +1,146 @@ | |||
| # Command-Line Options | |||
|
|
|||
| Both of Viper's verification backends can be configured via command-line options. When running a backend directly, the options are passed before the file to be verified, e.g., | |||
Member
There was a problem hiding this comment.
I think the only place that actually introduces the two backends is a single paragraph in the Introduction section? Maybe we should spell this out a bit more? We could do that here since (ideally) apart from just switching between SE/VCG in the IDE drop-down, the users don't need to know much about the backends. I would add the command-line invocation for Carbon as well or link to the scripts we have in the two repositories to give some context regarding where this invocation even came from.
|
|
||
| | Option | Description | | ||
| | ---- | ---- | | ||
| | `--counterexample <mode>` | Report a counterexample for each verification error. `resolved` yields a human-readable, backend-independent counterexample, in which heap resources are associated with the AST nodes they belong to; `raw` yields a backend-independent counterexample in which heap resources are keyed by backend-internal identifiers. The legacy modes `native` (the SMT solver's raw model), `variables` (values of all local Viper variables) and `mapped` (SE backend only) are also supported. | |
Member
There was a problem hiding this comment.
Are we deprecating the "legacy" modes?
| | Option | Description | | ||
| | ---- | ---- | | ||
| | `--counterexample <mode>` | Report a counterexample for each verification error. `resolved` yields a human-readable, backend-independent counterexample, in which heap resources are associated with the AST nodes they belong to; `raw` yields a backend-independent counterexample in which heap resources are keyed by backend-internal identifiers. The legacy modes `native` (the SMT solver's raw model), `variables` (values of all local Viper variables) and `mapped` (SE backend only) are also supported. | | ||
| | `--select <names>` | Verify only the given comma-separated methods, functions and predicates (e.g., `--select m1,f2,P`), together with the declarations they depend on. All other parts of the program are ignored. | |
Member
There was a problem hiding this comment.
What does "ignored" mean exactly? I guess for each of the three kinds of items it means rather that it is made abstract, but we still keep the specifications for functions and methods?
|
|
||
| | Option | Description | | ||
| | ---- | ---- | | ||
| | `--timeout <n>` | Abort verification after approximately `n` seconds. The timeout applies to the whole verification run, not to individual methods (default: 0, i.e., no timeout). | |
Member
There was a problem hiding this comment.
Nit: it is slightly strange that --timeout is included in both Silicon- and Carbon-specific sections. I guess the reason is that its meaning is subtly different?
| | ---- | ---- | | ||
| | `--timeout <n>` | Abort verification after approximately `n` seconds. The timeout applies to the whole verification run, not to individual methods (default: 0, i.e., no timeout). | | ||
| | `--assertTimeout <n>` | Timeout in milliseconds for each SMT query that checks a proof obligation (default: no timeout). If the solver times out, the assertion is reported as failing. Setting this option can turn non-terminating or very slow verification attempts into (possibly spurious) errors. | | ||
| | `--checkTimeout <n>` | Timeout in milliseconds for internal SMT queries that do not directly correspond to proof obligations, e.g., queries that check whether a branch is infeasible or whether two references alias (default: 10). Increasing this value can make verification more complete at the cost of performance. | |
Member
There was a problem hiding this comment.
Can this timeout also be turned off, by providing a value of zero?
|
|
||
| | Option | Description | | ||
| | ---- | ---- | | ||
| | `--exhaleMode <n>` | How permissions are removed when exhaling (and when evaluating expressions that require permissions). `0` (default) is a greedy mode that is fast, but can fail if the required permission is split across several heap chunks that may or may not alias. `1` uses a more complete algorithm that sums up permissions from all potentially-aliasing chunks. `2` uses the greedy mode first and retries with the more complete algorithm only if verification fails. In the SE backend, `--counterexample` requires mode 1. | |
Member
There was a problem hiding this comment.
(Should we give them names rather than magic numbers at some point?)
We also should not need to say "In the SE backend", since we are already in the Silicon-specific section.
| | `--moreJoins <n>` | Whether to join execution paths after branching instead of verifying the rest of the method separately for each path. `0` (default) never joins, `1` joins branches resulting from impure conditionals (e.g., `b ==> acc(x.f)`), and `2` joins whenever possible. Joining can drastically reduce the number of paths in methods with many branches, but yields larger SMT queries. | | ||
| | `--maskHeapMode` | Use an alternative heap encoding based on total heap and permission maps (similar to the encoding of the VCG backend) rather than heap chunks. Not compatible with several other options, e.g., `--exhaleMode` and `--counterexample`. | | ||
| | `--simplifyOnConsume` | In `--maskHeapMode`, simplify the permission mask whenever permissions are removed, rather than just recording the subtraction. Only supported in combination with `--maskHeapMode`. | | ||
| | `--stateConsolidationMode <n>` | How eagerly the verifier merges heap chunks and derives facts from the current permissions (e.g., non-aliasing). `0` does minimal work, `1` (default) does the most work and is the most complete; the remaining modes are less eager variants (most of which consolidate only when retrying after a failure) and a mode intended for use with `--exhaleMode 1`. Run with `--help` for a description of all modes. | |
Member
There was a problem hiding this comment.
This is the documentation of the CLI options -- we should spell out the descriptions that you would get if you did run the tool with --help.
| | `--enableSimplifiedUnfolds` | When verifying a predicate's well-formedness, record the resulting symbolic heap and assumptions for each branch of its body, and reuse them whenever the predicate is unfolded (via an `unfold` statement or an `unfolding` expression) instead of processing the body again. This can speed up programs with complex predicate bodies. | | ||
| | `--recursivePredicateUnfoldings <n>` | How many nested `unfolding` expressions are evaluated in the bodies of recursive predicates (default: 1). | | ||
| | `--alternativeFunctionVerificationOrder` | Compute the order in which functions are verified (and in which their definitional axioms become available) in a way that also takes dependencies between functions via predicate unfoldings into account. This is more complete for some programs, but less complete for others. | | ||
| | `--disableShortCircuitingEvaluations` | Disable short-circuiting evaluation of `&&` and `||` during well-definedness checks. For example, checking `i > 0 && f(i)` then fails if the precondition of `f` requires `i > 0`. | |
Member
There was a problem hiding this comment.
Did you check if this line in the table renders correctly in mdbook? If not, you might have to spell out the disjunction operator as, e.g., <code>||</code>.
| | `--prover <name>` | The SMT solver to use: `Z3` (default; Z3 run as a separate process), `cvc5`, or `Z3-API` (Z3 accessed via its Java API instead of a separate process). | | ||
| | `--z3Exe <path>` | Path to the Z3 executable used by Boogie. Alternatively, the environment variable `Z3_EXE` can be set. | | ||
| | `--cvc5Exe <path>` | Path to the cvc5 executable. Alternatively, the environment variable `CVC5_EXE` can be set. | | ||
| | `--proverConfigArgs "<k>=<v> ..."` | SMT solver configuration options, given as space-separated `key=value` pairs, e.g., `--proverConfigArgs "smt.qi.eager_threshold=100"`. These override the options the SE backend sets by default. | |
Member
There was a problem hiding this comment.
What are the options it sets by default?
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.