man boogie (1): 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.