--- name: "boogie" section: "1" platform: "linux" package: "boogie" version: "2.4.1+dfsg-0.1" release: "Debian 12 (Bookworm)" platforms: ["linux"] url: "https://new.carta.tech/boogie" --- # boogie(1) compiler for the Boogie programming language ## 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)](/dot/1.md) 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 *n*th 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. - **/proverShutdownLimit***n* 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 **LET**s in Z3. Accepted values for *n* are: - **0** Do not use **LET**s. - **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)](/dot/1.md) ## 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.