Man pages sections > man1 > boogie

boogie - compiler for the Boogie programming language

boogie(1) Boogie boogie(1)

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 Af × (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) Boogie is copyright © 2003-2015 Microsoft Corporation and licensed under the Microsoft Public License <https://msdn.microsoft.com/en-us/library/ff647676.aspx>.
 
This manual page is copyright © 2013, 2015-2016 Benjamin Barenblat and licensed under the Apache License, Version 2.0.
2016-08-17 Git snapshot 1f2d6c1