Provided by: boogie_2.4.1+dfsg-0.1_all 
NAME
boogie - compiler for the Boogie programming language
SYNOPSIS
boogie [options] file.bpl ...
DESCRIPTION
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.
OPTIONS
boogie accepts a number of different types of options.
File macros
A number of boogie options accept a file argument, which may contain the following macros:
@FILE@ Expands to the last filename specified on the command line.
@PREFIX@
Expands to the concatenation of strings given by /logPrefix options.
@TIME@ Expands to the current time.
General options
/env:n Control printing of command-line arguments. Accepted values for n are:
0 Suppress printing of command-line arguments.
1 (default) Print command-line arguments during BPL print and prover log.
2 Print command-line arguments during BPL print and prover log, and also to
standard output.
/noLogo
Suppress printing of the version number and copyright message.
/wait Wait for a carriage return from the keyboard before exiting.
/xml:file
Also produce output in XML format to file.
Boogie options
Multiple .bpl files supplied on the command line are concatenated into one Boogie program.
/enhancedErrorMessages:n
Control printing of enhanced error messages. Accepted values for n are:
0 (default) Do not print enhanced error messages.
1 Print Z3 error model enhanced error messages.
/loopUnroll:n
Unroll loops, following up to n back edges (and then some).
/mv:file
Save the model in BVD format to the specified file.
/noResolve
Parse only.
/noTypecheck
Parse and resolve only.
/overlookTypeErrors
Skip any implementation with resolution or type checking errors.
/print:file
Print Boogie program to the specified file after parsing it. Specify /print:- to
print to standard output.
/printCFG:prefix
Print the control flow graph of each implementation in dot(1) format to files named
prefix.procedurename.dot.
/printDesugared
With /print, desugar calls.
/printModel:n
Control printing of Z3's error model. Accepted values for n are:
0 (default) Do not print Z3's error model.
1 Print Z3's error model.
2 Print Z3's error model and reverse mappings.
3 Print Z3's error model in a more human-readable way.
/printModelToFile:file
With /print, print Z3's error model to file instead of standard output.
/printUnstructured
With /print, desugar all structured statements.
/printWithUniqueIds
Print augmented information that uniquely identifies variables.
/proc:p
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".
/soundLoopUnrolling
Enable sound loop unrolling.
/useBaseNameForFileName
When parsing, use the base name of the file for tokens instead of the path supplied
on the command line.
Inference options
/checkInfer
Instrument inferred invariants as asserts to be checked by the theorem prover.
/contractInfer
Perform procedure contract inference.
/infer[:domains]
Use abstract interpretation to infer invariants. domains may be any of the
following:
c constant propagation
d dynamic type
i intervals
j stronger intervals (cannot be combined with other domains)
n nullness
p polyhedra for linear inequalities
t trivial bottom/top lattice (cannot be combined with other domains)
You may also specify the following options as pseudo-domains:
s debug statistics
0...9 number of iterations before applying a widen (default: 0)
The default is /infer:i. With /infer (and no domains), all domains will be used.
/instrumentInfer:flag
Control when inferred invariants are instrumented. Accepted values for flag are:
h (default) Instrument inferred invariants only at the beginning of loop
headers.
e Instrument inferred invariants at the beginning and end of every block.
This mode is intended for use in debugging abstract domains.
/noinfer
Turn off the default inference, and override any previous /infer flags.
/printInstrumented
Print Boogie program after it has been instrumented with invariants.
Debugging and tracing options
/break Launch and break into the debugger.
/log[:method]
Print debug output during translation.
/trace Blurt out various debug trace information. Implies /tracePOs.
/tracePOs
Output information about the number of proof obligations.
/traceTimes
Output timing information at certain points in the pipeline.
Verification condition generation options
/alwaysAssumeFreeLoopInvariants
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).
/causalImplies
Translate Boogie's A ==> B into prover's A ==> A && B.
/coalesceBlocks:n
Control when to coalesce blocks. Accepted values for n are:
0 Do not coalesce blocks.
1 (default) Coalesce blocks.
/fixedPointEngine:engine
Use the specified fixed point engine for inference.
/inferLeastForUnsat:prefix
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. Implies /stratifiedInline:1.
/inline:strategy
Use the specified inlining strategy for procedures with the :inline attribute.
Accepted strategies are none, assume (the default), assert, and spec.
/lazyInline:1
Use the lazy inlining algorithm.
/liveVariableAnalysis:n
Control when and how to perform live variable analysis. Accepted values for n are:
0 Do not perform live variable analysis.
1 (default) Perform live variable analysis.
2 Perform interprocedural live variable analysis.
/monomorphize
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.
/noVerify
Skip verification condition generation and invocation of the theorem prover.
/printInlined
Print the implementation after inlining calls to procedures with the :inline
attribute.
/recursionBound:n
Set the recursion bound for stratified inlining to n. By default, n is 500.
/reflectAdd
In the verification condition, generate an auxiliary symbol, elsewhere defined to
be +, instead of +.
/removeEmptyBlocks:n
Control whether to remove empty blocks during verification condition generation.
Accepted values for n are:
0 Do not remove empty blocks.
1 (default) Remove empty blocks.
/smoke Run the soundness smoke test: try to stick assert false; in some places in the BPL
and see if we can still prove it.
/smokeTimeout:n
Set the timeout, in seconds, for a single theorem prover invocation during the
smoke test. By default, n is 10.
/stratifiedInline:1
Use the stratified inlining algorithm.
/subsumption:n
Control when subsumption is applied to asserted conditions. Accepted values for n
are:
0 Never apply subsumption.
1 Do not apply subsumption for quantifiers.
2 (default) Always apply subsumption.
/traceverify
Print debug output during verification condition generation.
/typeEncoding:method
Control how to encode types when sending the verification condition to the the
theorem prover. Allowed methods are:
a arguments
m monomorphic
n none (unsound)
p (default) predicates
/vc:variety
Specify the verification condition variety. Accepted varieties are:
b flat block
d (default) DAG
doomed doomed
l local
m nested block reach
n nested block
r flat block reach
s structured
/verifySeparately
Verify each input program separately.
/verifySnapshots:n
Verify several program snapshots (named filename.v0.bpl to filename.vN.bpl),
possibly using verification result caching. Accepted values for n are:
0 (default) Do not use any verification result caching.
1 Use basic verification result caching.
2 Use advanced verification result caching.
3 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
/vcsCores:n
Try to verify n verification conditions at once. Defaults to 1.
/vcsDumpSplits
For the nth split, dump split.n.dot and split.n.bpl. Note that this affects error
reporting.
/vcsFinalAssertTimeout:n
Set the timeout, in seconds, for the single last assertion in keep-going mode. By
default, n is 30.
/vcsKeepGoingTimeout:n
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.
/vcsLoad:f
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 1.
/vcsMaxCost:f
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 splitting.
/vcsMaxKeepGoingSplits:n
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).
/vcsMaxSplits:n
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 formula
(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 1.0.
/vcsPathJoinMult:f
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.
/vcsPathSplitMult:f
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.
Prover options
/errorLimit:n
Limit the number of errors produced for each procedure. By default, n is 5, but
some provers may only support 1.
/errorTrace:n
Control whether or not trace labels appear in the error output. Accepted values
for n are:
0 Print no trace labels in the error output.
1 (default) Print useful trace labels in error output.
2 Print all trace labels in error output.
/logPrefix:prefix
Define the expansion of the macro @PREFIX@.
/p:key[:value], /proverOpt:key[:value]
Provide a prover-specific option.
/platform:ptype,location
Set the platform type and location. ptype may be v11, v2, or cli1, and location
should be the platform libraries directory.
/prover:p
Use theorem prover p. p may be a full path to a prover DLL, or it may be one of
the following standard provers:
ContractInference
Simplify
This implies /vc:n and /vcBrackets:1.
SMTLib (default) Use the SMTLib2 format, and call Z3.
Z3 Z3 with the Simplify format.
Z3api Z3 with the managed (CLI) API.
/proverLog:file
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.
/proverLogAppend
Append (do not overwrite) the specified prover log file.
/proverMemorylimit:n
Limit the prover to n megabytes of virtual memory before forcing it to restart. n
defaults to 100.
/proverShutdownLimitn
Set the time, in seconds, between closing the stream to the prover and killing the
prover process. n defaults to 0.
/proverWarnings:n
Control warning output from the prover. Accepted values for n are:
0 (default) Don't print warning output from the prover.
1 Print warnings to standard output.
2 Print warnings to standard error.
/restartProver
Restart the prover after each query.
/timeLimit:n
Limit the number of seconds spent trying to verify each procedure.
/vcBrackets:n
Control whether or not odd-charactered identifier names will be bracketed with pipe
characters ('|'). Accepted values for n are:
0 (default) Do not bracket odd-charactered identifier names.
1 Bracket odd-charactered identifier names.
Prover options (Simplify)
/simplifyMatchDepth:n
Set Simplify's matching depth limit.
Prover options (Z3)
/useArrayTheory
Use Z3's native array theory, as opposed to axioms. Implies /monomorphize.
/useSmtOutputFormat
Output a model in SMTLib2 format.
/z3exe:path
Set the path to the Z3 executable. On Debian systems, this defaults to
/usr/bin/z3.
/z3lets:n
Configure use of LETs in Z3. Accepted values for n are:
0 Do not use LETs.
1 Use only LET TERM.
2 Use only LET FORMULA.
3 (default) Use any LET.
/z3multipleErrors
Report multiple counterexamples for each error.
/z3opt:option
Set an additional Z3 option.
/z3types
Generate a multi-sorted verification condition that makes use of Z3 types.
SEE ALSO
dot(1)
COPYRIGHT
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.