boogie - compiler for the Boogie programming language
boogie [options] file.bpl ...
boogie is a compiler for Microsoft Research's Boogie programming
language, an imperative compiler intermediate language with built-in
specification constructs. The integrated static analyzer can verify functional
correctness as part of the compilation process.
boogie accepts a number of different types of options.
A number of boogie options accept a file argument, which may
contain the following macros:
- Expands to the last filename specified on the command line.
- Expands to the concatenation of strings given by /logPrefix
- Expands to the current time.
- Control printing of command-line arguments. Accepted values
for n are:
- Suppress printing of command-line arguments.
- (default) Print command-line arguments during BPL print and prover
- Print command-line arguments during BPL print and prover log, and also to
- Suppress printing of the version number and copyright message.
- Wait for a carriage return from the keyboard before exiting.
- Also produce output in XML format to file.
Multiple .bpl files supplied on the command line are concatenated into one
- Control printing of enhanced error messages. Accepted values
for n are:
- (default) Do not print enhanced error messages.
- Print Z3 error model enhanced error messages.
- Unroll loops, following up to n back edges (and then some).
- Save the model in BVD format to the specified file.
- Parse only.
- Parse and resolve only.
- Skip any implementation with resolution or type checking errors.
- Print Boogie program to the specified file after parsing it. Specify
/print:- to print to standard output.
- Print the control flow graph of each implementation in dot(1)
format to files named prefix.procedurename.dot.
- With /print, desugar calls.
- Control printing of Z3's error model. Accepted values for n
- (default) Do not print Z3's error model.
- Print Z3's error model.
- Print Z3's error model and reverse mappings.
- Print Z3's error model in a more human-readable way.
- With /print, print Z3's error model to file instead of
- With /print, desugar all structured statements.
- Print augmented information that uniquely identifies variables.
- Only check procedures matched by the pattern p. This option may be
specified multiple times to match multiple patterns. The pattern p
matches the whole procedure name (e.g., a pattern "foo" will
only match a procedure called "foo", not one called
"fooBar"). The pattern p may contain * wildcards which
match any character zero or more times. For example, the pattern
"ab*d" would match "abd", "abcd", and
"abccd", but not "Aabd" or "abdD". The
pattern "*ab*d*" would match "abd", "abcd",
"abccd", "Abd", and "abdD".
- Enable sound loop unrolling.
- When parsing, use the base name of the file for tokens instead of the path
supplied on the command line.
- Instrument inferred invariants as asserts to be checked by the theorem
- Perform procedure contract inference.
- Use abstract interpretation to infer invariants. domains may be any
of the following:
- constant propagation
- dynamic type
- stronger intervals (cannot be combined with other domains)
- polyhedra for linear inequalities
- trivial bottom/top lattice (cannot be combined with other domains)
- You may also specify the following options as pseudo-domains:
- debug statistics
- number of iterations before applying a widen (default: 0)
- The default is /infer:i. With /infer (and no
domains), all domains will be used.
- Control when inferred invariants are instrumented. Accepted values
for flag are:
- (default) Instrument inferred invariants only at the beginning of loop
- Instrument inferred invariants at the beginning and end of every block.
This mode is intended for use in debugging abstract domains.
- Turn off the default inference, and override any previous /infer
- Print Boogie program after it has been instrumented with invariants.
Debugging and tracing options¶
- Launch and break into the debugger.
- Print debug output during translation.
- Blurt out various debug trace information. Implies /tracePOs.
- Output information about the number of proof obligations.
- Output timing information at certain points in the pipeline.
Verification condition generation options¶
- Include free loop invariants as assumptions in checking contexts. Usually,
a free loop invariant (or assume statement in that position) is ignored in
checking contexts (like other free things).
- Translate Boogie's A ==> B into prover's
A ==> A && B.
- Control when to coalesce blocks. Accepted values for n
- Do not coalesce blocks.
- (default) Coalesce blocks.
- Use the specified fixed point engine for inference.
- Infer the least number of constants (whose names are prefixed by
prefix) that need to be set to true for the program to be correct.
- Use the specified inlining strategy for procedures with the :inline
attribute. Accepted strategies are none, assume (the
default), assert, and spec.
- Use the lazy inlining algorithm.
- Control when and how to perform live variable analysis. Accepted values
for n are:
- Do not perform live variable analysis.
- (default) Perform live variable analysis.
- Perform interprocedural live variable analysis.
- Do not abstract map types in the encoding. This is an experimental feature
which will not do the right thing if the program uses polymorphism.
- Skip verification condition generation and invocation of the theorem
- Print the implementation after inlining calls to procedures with the
- Set the recursion bound for stratified inlining to n. By default,
n is 500.
- In the verification condition, generate an auxiliary symbol, elsewhere
defined to be +, instead of +.
- Control whether to remove empty blocks during verification condition
generation. Accepted values for n are:
- Do not remove empty blocks.
- (default) Remove empty blocks.
- Run the soundness smoke test: try to stick assert false; in some
places in the BPL and see if we can still prove it.
- Set the timeout, in seconds, for a single theorem prover invocation during
the smoke test. By default, n is 10.
- Use the stratified inlining algorithm.
- Control when subsumption is applied to asserted conditions. Accepted
values for n are:
- Never apply subsumption.
- Do not apply subsumption for quantifiers.
- (default) Always apply subsumption.
- Print debug output during verification condition generation.
- Control how to encode types when sending the verification condition to the
the theorem prover. Allowed methods are:
- none (unsound)
- (default) predicates
- Specify the verification condition variety. Accepted varieties are:
- flat block
- (default) DAG
- nested block reach
- nested block
- flat block reach
- Verify each input program separately.
- Verify several program snapshots (named filename.v0.bpl to
filename.vN.bpl), possibly using verification result caching.
Accepted values for n are:
- (default) Do not use any verification result caching.
- Use basic verification result caching.
- Use advanced verification result caching.
- Use advanced verification result caching, and report errors according to
the new source locations for errors and their related locations (but not
/errorTrace and CaptureState locations).
Verification condition splitting¶
- Try to verify n verification conditions at once. Defaults to
- For the nth split, dump split.n.dot and
split.n.bpl. Note that this affects error reporting.
- Set the timeout, in seconds, for the single last assertion in keep-going
mode. By default, n is 30.
- Set the timeout, in seconds, for a single theorem prover invocation in
keep-going mode, except for the final single-assertion case. By default,
n is 1.
- Like /vcsCores:n, where n is the machine's processor
count multiplied by f and rounded to the nearest integer. f
must be in the range [0.0, 3.0]. This will never set n less than
- Verification conditions will not be split unless the cost of a
verification condition exceeds f. f defaults to 2000.0. This
does not apply in the keep-going mode after the first round of
- If n is set to more than 1, this activates keep-going mode, where
after the first round of splitting, verification conditions that time out
are split into n pieces and retried until either proving them is
successful or there is only one assertion on a single path and it times
out. (In such a case, boogie reports an error for that assertion).
By default, n is 1 (that is, keep-going mode is disabled).
- Set the maximal number of verification conditions generated per method. In
keep-going mode, this only applies to the first round. By default,
n is 1.
- /vcsPathCostMult:f1, /vcsAssumeMult:f2
- Controls the cost of a block. Block cost is computed according to the
(assert-cost + f2 × assume-cost) × (1 +
f1 × entering-paths)
- where f1 defaults to 1.0 and f2 defaults
to 0.01. The cost of a single assertion or assumption is always
- Sets a scale factor which boogie will multiply by the number of
paths in a block if more than one path join at a block. This is intended
to reflect the fact that the prover will learn something on one path
before proceeding to the next. By default, f is 0.8.
- If the best path split of a verification condition of cost A is
into verification conditions of cost B and C,
then the split is applied if A ≥ f × (B
+ C). Otherwise, assertion splitting will be applied. By default,
f is 0.5 (that is, always do path splitting if possible). Increase
f to do less path splitting and more assertion splitting.
- Limit the number of errors produced for each procedure. By default,
n is 5, but some provers may only support 1.
- Control whether or not trace labels appear in the error output. Accepted
values for n are:
- Print no trace labels in the error output.
- (default) Print useful trace labels in error output.
- Print all trace labels in error output.
- Define the expansion of the macro @PREFIX@.
- Provide a prover-specific option.
- Set the platform type and location. ptype may be v11,
v2, or cli1, and location should be the platform
- Use theorem prover p. p may be a full path to a prover DLL,
or it may be one of the following standard provers:
- This implies /vc:n and /vcBrackets:1.
- (default) Use the SMTLib2 format, and call Z3.
- Z3 with the Simplify format.
- Z3 with the managed (CLI) API.
- Log input for the theorem prover.
- In addition to the standard file name macros, file can use the
@PROC@ macro, which causes boogie to generate one prover log
file per verification condition, expanding @PROC@ to the name of
the procedure that the verification condition is for.
- Append (do not overwrite) the specified prover log file.
- Limit the prover to n megabytes of virtual memory before forcing it
to restart. n defaults to 100.
- Set the time, in seconds, between closing the stream to the prover and
killing the prover process. n defaults to 0.
- Control warning output from the prover. Accepted values
for n are:
- (default) Don't print warning output from the prover.
- Print warnings to standard output.
- Print warnings to standard error.
- Restart the prover after each query.
- Limit the number of seconds spent trying to verify each procedure.
- Control whether or not odd-charactered identifier names will be bracketed
with pipe characters ('|'). Accepted values for n are:
- (default) Do not bracket odd-charactered identifier names.
- Bracket odd-charactered identifier names.
Prover options (Simplify)¶
- Set Simplify's matching depth limit.
Prover options (Z3)¶
- Use Z3's native array theory, as opposed to axioms. Implies
- Output a model in SMTLib2 format.
- Set the path to the Z3 executable. On Debian systems, this defaults to
- Configure use of LETs in Z3. Accepted values for n
- Do not use LETs.
- Use only LET TERM.
- Use only LET FORMULA.
- (default) Use any LET.
- Report multiple counterexamples for each error.
- Set an additional Z3 option.
- Generate a multi-sorted verification condition that makes use of Z3
Boogie is copyright © 2003-2015 Microsoft Corporation and licensed under
the Expat license.
This manual page is copyright © 2013, 2015-2016 Benjamin
Barenblat and licensed under the Expat license.