boogie1

File macros

A number of boogie options accept a file argument, which may contain the following macros:

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

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.