Provided by: boogie_188.8.131.52016+dfsg+3.gbp1f2d6c1-1_all
boogie - compiler for the Boogie programming language
boogie [options] file.bpl ...
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.
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.
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.