List of Configuration Flags

Name	Rust type	Default value	Multi-Crate Category
`ALLOW_UNREACHABLE_UNSUPPORTED_CODE`	`bool`	`false`	A
`ASSERT_TIMEOUT`	`u64`	`10_000`	A
`BE_RUSTC`	`bool`	`false`	B
`BOOGIE_PATH`	`Option<String>`	`env::var("BOOGIE_EXE")`	A
`CACHE_PATH`	`String`	`""`	A*
`CARGO_COMMAND`	`String`	`"check"`	B
`CARGO_PATH`	`String`	`"cargo"`	B
`CHECK_FOLDUNFOLD_STATE`	`bool`	`false`	A
`CHECK_OVERFLOWS`	`bool`	`true`	A
`CHECK_PANICS`	`bool`	`true`	A
`CHECK_TIMEOUT`	`Option<u32>`	`None`	A
`COUNTEREXAMPLE`	`bool`	`false`	A
`DELETE_BASIC_BLOCKS`	`Vec<String>`	`vec![]`	A
`DUMP_BORROWCK_INFO`	`bool`	`false`	A
`DUMP_DEBUG_INFO`	`bool`	`false`	A
`DUMP_DEBUG_INFO_DURING_FOLD`	`bool`	`false`	A
`DUMP_PATH_CTXT_IN_DEBUG_INFO`	`bool`	`false`	A
`DUMP_REBORROWING_DAG_IN_DEBUG_INFO`	`bool`	`false`	A
`DUMP_VIPER_PROGRAM`	`bool`	`false`	A
`ENABLE_CACHE`	`bool`	`true`	A
`ENABLE_PURIFICATION_OPTIMIZATION`	`bool`	`false`	A
`ENABLE_TYPE_INVARIANTS`	`bool`	`false`	A
`ENABLE_VERIFY_ONLY_BASIC_BLOCK_PATH`	`bool`	`false`	A
`ENCODE_BITVECTORS`	`bool`	`false`	A
`ENCODE_UNSIGNED_NUM_CONSTRAINT`	`bool`	`false`	A
`EXTRA_JVM_ARGS`	`Vec<String>`	`vec![]`	A
`EXTRA_VERIFIER_ARGS`	`Vec<String>`	`vec![]`	A
`FOLDUNFOLD_STATE_FILTER`	`String`	`""`	A
`FULL_COMPILATION`	`bool`	`false`	A*
`HIDE_UUIDS`	`bool`	`false`	A
`IGNORE_REGIONS`	`bool`	`false`	A
`INTERNAL_ERRORS_AS_WARNINGS`	`bool`	`false`	A
`INTERN_NAMES`	`bool`	`true`	A
`JAVA_HOME`	`Option<String>`	`None`	A
`JSON_COMMUNICATION`	`bool`	`false`	A
`LOG`	`String`	`""`	A
`LOG_DIR`	`String`	`"log"`	A*
`LOG_STYLE`	`String`	`"auto"`	A
`LOG_SMT_WRAPPER_INTERACTION`	`bool`	`false`	A
`LOG_TRACING`	`bool`	`true`	A
`MAX_LOG_FILE_NAME_LENGTH`	`usize`	`60`	A
`MIN_PRUSTI_VERSION`	`Option<String>`	`None`	A
`VERIFY_MODE`	`String`	`verify`	A
`NO_VERIFY_DEPS`	`bool`	`false`	B
`IGNORE_DEPS_CONTRACTS`	`bool`	`false`	B
`OPT_IN_VERIFICATION`	`bool`	`false`	A
`OPTIMIZATIONS`	`Vec<String>`	"all"	A
`PRESERVE_SMT_TRACE_FILES`	`bool`	`false`	A
`PRINT_COLLECTED_VERIFICATION_ITEMS`	`bool`	`false`	A
`PRINT_COUNTEREXAMPLE_IF_MODEL_IS_PRESENT`	`bool`	`false`	A
`PRINT_DESUGARED_SPECS`	`bool`	`false`	A
`PRINT_TYPECKD_SPECS`	`bool`	`false`	A
`QUERY_METHOD_SIGNATURE`	`Option<String>`	`None`	A
`QUIET`	`bool`	`false`	A*
`REPORT_VIPER_MESSAGES`	`bool`	`false`	A
`REPORT_BLOCK_MESSAGES`	`bool`	`false`	A
`SERVER_ADDRESS`	`Option<String>`	`None`	A
`SERVER_MAX_CONCURRENCY`	`Option<usize>`	`None`	A
`SERVER_MAX_STORED_VERIFIERS`	`Option<usize>`	`None`	A
`SHORT_VIPER_NAMES`	`bool`	`false`	A
`SHOW_IDE_INFO`	`bool`	`false`	A
`SIMPLIFY_ENCODING`	`bool`	`true`	A
`SKIP_UNSUPPORTED_FEATURES`	`bool`	`false`	A
`SKIP_VERIFICATION`	`bool`	`false`	A
`SMT_QI_BOUND_GLOBAL`	`Option<u64>`	`None`	A
`SMT_QI_BOUND_GLOBAL_KIND`	`Option<u64>`	`None`	A
`SMT_QI_BOUND_TRACE`	`Option<u64>`	`None`	A
`SMT_QI_BOUND_TRACE_KIND`	`Option<u64>`	`None`	A
`SMT_QI_EAGER_THRESHOLD`	`u64`	`1000`	A
`SMT_QI_IGNORE_BUILTIN`	`bool`	`true`	A
`SMT_QI_PROFILE`	`Option<bool>`	`None`	A
`SMT_QI_PROFILE_FREQ`	`Option<u64>`	`None`	A
`SMT_SOLVER_PATH`	`Option<String>`	`env::var("Z3_EXE")`	A
`SMT_SOLVER_WRAPPER_PATH`	`Option<String>`	`None`	A
`SMT_UNIQUE_TRIGGERS_BOUND`	`Option<u64>`	`None`	A
`SMT_UNIQUE_TRIGGERS_BOUND_TOTAL`	`Option<u64>`	`None`	A
`UNSAFE_CORE_PROOF`	`bool`	`false`	A
`USE_MORE_COMPLETE_EXHALE`	`bool`	`true`	A
`USE_SMT_WRAPPER`	`bool`	`false`	A
`VERIFICATION_DEADLINE`	`Option<u64>`	`None`	A
`VERIFY_ONLY_BASIC_BLOCK_PATH`	`Vec<String>`	`vec![]`	A
`VERIFY_ONLY_DEFPATH`	`Vec<String>`	`vec![]`	A
`VERIFY_ONLY_PREAMBLE`	`bool`	`false`	A
`VIPER_BACKEND`	`String`	`"Silicon"`	A
`VIPER_HOME`	`Option<String>`	`None`	A
`WRITE_SMT_STATISTICS`	`bool`	`false`	A

`ALLOW_UNREACHABLE_UNSUPPORTED_CODE`

When enabled, unsupported code is encoded as assert false. This way error messages are reported only for unsupported code that is actually reachable.

`ASSERT_TIMEOUT`

Maximum time (in milliseconds) for the verifier to spend on a single assertion. Set to 0 to disable timeout. Maps to the verifier command-line argument --assertTimeout.

`BE_RUSTC`

When enabled, Prusti will behave like rustc.

Note: applied to all dependency crates when running with cargo prusti.

`BOOGIE_PATH`

A path to Boogie.

Note: prusti-rustc sets this option.

Path to a cache file, where verification cache will be loaded from and saved to. The default empty string disables saving any cache to disk. A path to a file which does not yet exist will result in using an empty cache, but then creating and saving to that location on exit.

Note: cargo prusti sets this flag with DEFAULT_PRUSTI_CACHE_PATH=$CARGO_TARGET_DIR/cache.bin.

`CARGO_COMMAND`

The cargo command to run when checking a crate with cargo prusti. Change to build to export binaries, library files and specs.

Note: Applicable only under cargo prusti.

`CARGO_PATH`

The path to cargo when running cargo prusti. Useful if cargo is not available in the path.

Note: Applicable only under cargo prusti.

`CHECK_FOLDUNFOLD_STATE`

When enabled, additional, slow, checks for the fold/unfold algorithm will be generated.

`CHECK_OVERFLOWS`

When enabled, binary operations and numeric casts will be checked for overflows. See integer type encoding.

`CHECK_PANICS`

When enabled, Prusti will check for an absence of panic!s.

`CHECK_TIMEOUT`

Maximum time (in milliseconds) for the verifier to spend on checks. Set to None uses the verifier's default value. Maps to the verifier command-line argument --checkTimeout. For more information see here.

`COUNTEREXAMPLE`

When enabled, Prusti will try to find and print a counterexample for any failed assertion or specification.

`DELETE_BASIC_BLOCKS`

The given basic blocks will be replaced with assume false.

`DUMP_BORROWCK_INFO`

When enabled, borrow checking info will be output.

`DUMP_DEBUG_INFO`

When enabled, debug files will be created.

`DUMP_DEBUG_INFO_DURING_FOLD`

When enabled, the state of the fold-unfold algorithm after each step will be dumped to a file.

`DUMP_PATH_CTXT_IN_DEBUG_INFO`

When enabled, branch context state will be output in debug files.

`DUMP_REBORROWING_DAG_IN_DEBUG_INFO`

When enabled, reborrowing DAGs will be output in debug files.

`DUMP_VIPER_PROGRAM`

When enabled, the encoded Viper programs will be output. You can find them either in log/viper_program or target/verify/log/viper_program.

`ENABLE_CACHE`

When enabled, verification requests (to verify individual fns) are cached to improve future verification. By default the cache is only saved in memory (of the prusti-server if enabled). For long-running verification projects use CACHE_PATH to save to disk.

`ENABLE_PURIFICATION_OPTIMIZATION`

When enabled, impure methods are optimized using the purification optimization, which tries to convert heap operations to pure (snapshot-based) operations.

Note: This option is highly experimental.

`ENABLE_TYPE_INVARIANTS`

When enabled, type invariants can be declared on types using the #[invariant(...)] attribute.

`ENABLE_VERIFY_ONLY_BASIC_BLOCK_PATH`

When enabled, only the path given in VERIFY_ONLY_BASIC_BLOCK_PATH will be verified.

Note: This flag is only for debugging Prusti.

`ENCODE_BITVECTORS`

When enabled, bitwise integer operations are encoded using bitvectors.

Note: This option is highly experimental.

`ENCODE_UNSIGNED_NUM_CONSTRAINT`

When enabled, non-negativity of unsigned integers will be encoded and checked.

`EXTRA_JVM_ARGS`

Additional arguments to pass to the JVM when launching a verifier backend.

`EXTRA_VERIFIER_ARGS`

Additional arguments to pass to the verifier backend.

`FOLDUNFOLD_STATE_FILTER`

Filter for fold/unfold nodes when debug info is dumped.

`FULL_COMPILATION`

When enabled, compilation will continue and a binary will be generated after Prusti terminates.

Note: cargo prusti sets this flag with DEFAULT_PRUSTI_FULL_COMPILATION=true.

`HIDE_UUIDS`

When enabled, UUIDs of expressions and specifications printed with PRINT_TYPECKD_SPECS are hidden.

`IGNORE_REGIONS`

When enabled, debug files dumped by rustc will not contain lifetime regions.

`INTERNAL_ERRORS_AS_WARNINGS`

When enabled, internal errors are presented as warnings.

Note: This should only be used for debugging, as enabling this setting could hide actual verification errors.

`INTERN_NAMES`

When enabled, Viper identifiers are interned to shorten them when possible.

`JAVA_HOME`

The path the directory containing Java.

Note: prusti-rustc sets this option.

`JSON_COMMUNICATION`

When enabled, communication with the server will be encoded as JSON instead of the default bincode.

`LOG`

Log level and filters. See env_logger documentation.

For example, PRUSTI_LOG=prusti_viper=trace enables trace logging for the prusti-viper crate, or PRUSTI_LOG=debug enables lighter logging everywhere. When using trace it is recommended to disable jni messages with e.g. PRUSTI_LOG=trace,jni=warn. A useful explanation of this can be found in the rustc docs (we set PRUSTI_LOG rather than RUSTC_LOG). When running prusti-rustc and prusti-server, it is possible to report log messages to stderr, however in release builds all trace and most debug logs are not available.

`LOG_DIR`

Path to directory in which log files and dumped output will be stored.

Note: cargo prusti sets this flag with DEFAULT_PRUSTI_LOG_DIR=$CARGO_TARGET_DIR/log.

`LOG_STYLE`

Log style. See env_logger documentation. Has no effect when LOG_TRACING=true.

`LOG_SMT_WRAPPER_INTERACTION`

When enabled, logs all SMT wrapper interaction to a file.

Note: Requires USE_SMT_WRAPPER to be true.

`LOG_TRACING`

When enabled, logs are outputted using the tracing_chrome crate rather than as std output with the env_logger. You can find the file at $LOG_DIR/trace.json which can be opened in ui.perfetto.dev. The file is only generated if LOG is set.

`MAX_LOG_FILE_NAME_LENGTH`

Maximum allowed length of a log file name. If this is exceeded, the file name is truncated.

`MIN_PRUSTI_VERSION`

Minimum required version of Prusti that is allowed to run. If Prusti detects that its own version is lower than this, it will throw an error and refuse to verify files. Generally set in a Prusti.toml file of a crate to enforce a minimum Prusti version.

`VERIFY_MODE`

This flag defines which mode Prusti runs in:

compile-only: This only compiles the Rust program but does not encode it into Viper.
encode-only: This encodes the Rust program into Viper, without running Viper on it. The resulting Viper program may be inconsistent, even when Prusti returns no error. From this point on, the Viper program can be dumped by setting DUMP_VIPER_PROGRAM.
consistency-check: After encoding the Rust program into Viper, Prusti calls Viper to perform consistency checks on the Viper program, without actually verifying the program.
verify: This is the default option and used to verify the Viper program.

`NO_VERIFY_DEPS`

When enabled, verification is skipped for dependencies. Equivalent to setting VERIFY_MODE to compile-only for all dependencies. Remote dependencies from e.g. git/crates.io are already automatically set to compile-only.

Note: applied to all dependency crates when running with cargo prusti.

`IGNORE_DEPS_CONTRACTS`

When enabled, Prusti will not collect contracts from the project's dependencies. This is useful for debugging and working around unsupported language features in the dependencies.

`OPT_IN_VERIFICATION`

When enabled, Prusti will only try to verify the functions annotated with #[verified]. All other functions are assumed to be #[trusted], by default. Functions annotated with both #[trusted] and #[verified] will not be verified.

`ONLY_MEMORY_SAFETY`

When enabled, only the core proof is verified.

Note: This should be used only when UNSAFE_CORE_PROOF is enabled.

`OPTIMIZATIONS`

Comma-separated list of optimizations to enable, or "all" to enable all. Possible values in the list are:

"inline_constant_functions"
"delete_unused_predicates"
"optimize_folding"
"remove_empty_if"
"purify_vars"
"fix_quantifiers"
"fix_unfoldings"
"remove_unused_vars"
"remove_trivial_assertions"
"clean_cfg"

`PRESERVE_SMT_TRACE_FILES`

When enabled, does not delete Z3 trace files.

Note: Requires USE_SMT_WRAPPER to be true.

`PRINT_COLLECTED_VERIFICATION_ITEMS`

When enabled, prints the items collected for verification.

`PRINT_COUNTEREXAMPLE_IF_MODEL_IS_PRESENT`

When enabled, a counterexample contains values for the original type and its model.

`PRINT_DESUGARED_SPECS`

When enabled, prints the AST with desugared specifications.

`PRINT_TYPECKD_SPECS`

When enabled, prints the type-checked specifications.

`QUERY_METHOD_SIGNATURE`

When set to a defpath, prusti will generate a template for an external specification for this method. The result is part of the CompilerInfo and will only be emitted if the SHOW_IDE_INFO flag is enabled too.

`QUIET`

When enabled, user messages are not printed. Otherwise, messages output into stderr.

Note: cargo prusti sets this flag with DEFAULT_PRUSTI_QUIET=true.

`REPORT_VIPER_MESSAGES`

When enabled for both server and client, certain supported Viper messages will be reported to the user.

`REPORT_BLOCK_MESSAGES`

When enabled for both server and client, messages for individual basic blocks will be reported to the user. Does nothing if REPORT_VIPER_MESSAGES is not enabled. Intended for usage with the Prusti Assistant (IDE).

`SERVER_ADDRESS`

When set to an address and port (e.g. "127.0.0.1:2468"), Prusti will connect to the given server and use it for its verification backend.

When set to "MOCK", the server is run off-thread, effectively mocking connecting to a server without having to start it up separately.

`SERVER_MAX_CONCURRENCY`

Maximum amount of verification requests the server will work on concurrently. If not set, defaults to the number of (logical) cores on the system.

`SERVER_MAX_STORED_VERIFIERS`

Maximum amount of instantiated Viper verifiers the server will keep around for reuse. If not set, defaults to SERVER_MAX_CONCURRENT_VERIFICATION_OPERATIONS. It also doesn't make much sense to set this option to less than that, since then the server will likely have to keep creating new verifiers, reducing the performance gained from reuse.

Note: This does not limit how many verification requests the server handles concurrently, only the size of what is essentially its verifier cache.

`SHORT_VIPER_NAMES`

When enabled, Viper identifiers derived from Rust items use the item's short name (e.g. Foo) instead of its full definition path (e.g. my_crate::module::Foo). This is useful for debugging but may result in name collisions (in which case the generated Viper programs will fail to compile).

`SHOW_IDE_INFO`

When enabled, we emit various json data structures containing information about the program, its encoding, and the results of the verification. This flag intended for prusti-assistant (IDE).

`SIMPLIFY_ENCODING`

When enabled, the encoded program is simplified before it is passed to the Viper backend.

`SKIP_UNSUPPORTED_FEATURES`

When enabled, features not supported by Prusti will be reported as warnings rather than errors.

`SKIP_VERIFICATION`

When enabled, verification will be skipped. Opposed to VERIFY_MODE=compile-only, this flag will cause fake errors to stop the compiler from caching the result.

`SMT_QI_BOUND_GLOBAL`

If not None, checks that the number of global quantifier instantiations reported by the SMT wrapper is smaller than the specified bound.

Note: Requires USE_SMT_WRAPPER to be true.

`SMT_QI_BOUND_GLOBAL_KIND`

If not None, checks that the number of global quantifier instantiations for each quantifier reported by the SMT wrapper is smaller than the specified bound.

Note: Requires USE_SMT_WRAPPER to be true.

`SMT_QI_BOUND_TRACE`

If not None, checks that the number of quantifier instantiations in each trace reported by the SMT wrapper is smaller than the specified bound.

Note: Requires USE_SMT_WRAPPER to be true.

`SMT_QI_BOUND_TRACE_KIND`

If not None, checks that the number of quantifier instantiations in each trace for each quantifier reported by the SMT wrapper is smaller than the specified bound.

Note: Requires USE_SMT_WRAPPER to be true.

`SMT_QI_EAGER_THRESHOLD`

A threshold controlling how many times Z3 should instantiate a single quantifier. This option controls a tradeoff between performance and completeness:

Setting it to a too small value, may lead to spurious verification errors and unstable verification.

Setting it to a too large value, may significantly impact performance.

`SMT_QI_IGNORE_BUILTIN`

When enabled, ignores the built-in quantifiers in SMT quantifier instantiation bounds checking.

`SMT_QI_PROFILE`

When enabled, the Z3 backend periodically (and on finish) reports the number of quantifier instantiations to Viper.

`SMT_QI_PROFILE_FREQ`

Frequency of the quantifier instantiation reporting of Z3 (every X instantiations, a report is issued).

`SMT_SOLVER_PATH`

Path to Z3.

Note: prusti-rustc sets this option.

`SMT_SOLVER_WRAPPER_PATH`

A path to prusti-smt-solver.

Note: prusti-rustc sets this option.

`SMT_UNIQUE_TRIGGERS_BOUND`

If not None, checks that the number of unique triggers used for each quantifier reported by the SMT wrapper is smaller than the specified bound.

Note: Requires USE_SMT_WRAPPER to be true.

`SMT_UNIQUE_TRIGGERS_BOUND_TOTAL`

If not None, checks that the total number of unique triggers reported by the SMT wrapper is smaller than the specified bound.

Note: Requires USE_SMT_WRAPPER to be true.

`UNSAFE_CORE_PROOF`

When enabled, the new core proof is used, suitable for unsafe code

Note: This option is currently very incomplete.

`USE_MORE_COMPLETE_EXHALE`

When enabled, a more complete exhale version is used in the verifier. See consolidate. Equivalent to the verifier command-line argument --enableMoreCompleteExhale.

`USE_SMT_WRAPPER`

Whether to use the SMT solver wrapper. Enabling this is required to be able to use quantifier instantiation bounds checking.

This flag is intended to be used in tests only.

`VERIFICATION_DEADLINE`

Deadline (in seconds) within which Prusti should encode and verify the program.

Prusti panics if it fails to meet this deadline. This flag is intended to be used for tests that aim to catch performance regressions.

`VERIFY_ONLY_BASIC_BLOCK_PATH`

Verify only the single execution path goes through the given basic blocks. All basic blocks not on this execution path are replaced with assume false. Must be enabled using the ENABLE_VERIFY_ONLY_BASIC_BLOCK_PATH flag.

Note: This option is only for debugging Prusti.

`VERIFY_ONLY_DEFPATHS`

When set to the defpath of a local method, prusti will only verify the specified method. A fake error will be generated to avoid caching of a success.

Note: When passing this flag through environment variables, it should be a string of space-separated defpaths.

`VERIFY_ONLY_PREAMBLE`

When enabled, only the preamble will be verified: domains, functions, and predicates.

Note: With this flag enabled, no methods are verified!

`VIPER_BACKEND`

Verification backend to use. Possible values:

Carbon - verification-condition-generation-based backend Carbon.
Silicon - symbolic-execution-based backend Silicon.

`VIPER_HOME`

The path the directory containing the Viper JARs.

Note: prusti-rustc sets this option.

`WRITE_SMT_STATISTICS`

When enabled, dumps the statistics collected by the SMT wrapper into files next to the Z3 trace files.

Note: Requires USE_SMT_WRAPPER to be true.

Keyboard shortcuts

Prusti dev guide