Provided by: boogie_2.3.0.61016+dfsg+3.gbp1f2d6c1-1_all bug


       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.

              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.

              Suppress printing of the version number and copyright message.

       /wait  Wait for a carriage return from the keyboard before exiting.

              Also produce output in XML format to file.

   Boogie options
       Multiple .bpl files supplied on the command line are concatenated into one Boogie program.

              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.

              Unroll loops, following up to n back edges (and then some).

              Save the model in BVD format to the specified file.

              Parse only.

              Parse and resolve only.

              Skip any implementation with resolution or type checking errors.

              Print Boogie program to the specified file after parsing it.  Specify  /print:-  to
              print to standard output.

              Print the control flow graph of each implementation in dot(1) format to files named

              With /print, desugar calls.

              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.

              With /print, print Z3's error model to file instead of standard output.

              With /print, desugar all structured statements.

              Print augmented information that uniquely identifies variables.

              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".

              Enable sound loop unrolling.

              When parsing, use the base name of the file for tokens instead of the path supplied
              on the command line.

   Inference options
              Instrument inferred invariants as asserts to be checked by the theorem prover.

              Perform procedure contract inference.

              Use  abstract  interpretation  to  infer  invariants.   domains  may  be any of the

              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.

              Control when inferred invariants are instrumented.  Accepted values for flag are:

              h      (default) Instrument inferred invariants  only  at  the  beginning  of  loop

              e      Instrument  inferred  invariants  at  the  beginning and end of every block.
                     This mode is intended for use in debugging abstract domains.

              Turn off the default inference, and override any previous /infer flags.

              Print Boogie program after it has been instrumented with invariants.

   Debugging and tracing options
       /break Launch and break into the debugger.

              Print debug output during translation.

       /trace Blurt out various debug trace information.  Implies /tracePOs.

              Output information about the number of proof obligations.

              Output timing information at certain points in the pipeline.

   Verification condition generation options
              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).

              Translate Boogie's A ==> B into prover's A ==> A && B.

              Control when to coalesce blocks.  Accepted values for n are:

              0      Do not coalesce blocks.

              1      (default) Coalesce blocks.

              Use the specified fixed point engine for inference.

              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.

              Use  the  specified  inlining  strategy  for procedures with the :inline attribute.
              Accepted strategies are none, assume (the default), assert, and spec.

              Use the lazy inlining algorithm.

              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.

              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.

              Skip verification condition generation and invocation of the theorem prover.

              Print  the  implementation  after  inlining  calls  to  procedures with the :inline

              Set the recursion bound for stratified inlining to n.  By default, n is 500.

              In the verification condition, generate an auxiliary symbol, elsewhere  defined  to
              be +, instead of +.

              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.

              Set  the  timeout,  in  seconds,  for a single theorem prover invocation during the
              smoke test.  By default, n is 10.

              Use the stratified inlining algorithm.

              Control when subsumption is applied to asserted conditions.  Accepted values  for n

              0      Never apply subsumption.

              1      Do not apply subsumption for quantifiers.

              2      (default) Always apply subsumption.

              Print debug output during verification condition generation.

              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

              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

              Verify each input program separately.

              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
              Try to verify n verification conditions at once.  Defaults to 1.

              For  the nth split, dump and split.n.bpl.  Note that this affects error

              Set the timeout, in seconds, for the single last assertion in keep-going mode.   By
              default, n is 30.

              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.

              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.

              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.

              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).

              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.

              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.

              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
              Limit  the  number  of errors produced for each procedure.  By default, n is 5, but
              some provers may only support 1.

              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.

              Define the expansion of the macro @PREFIX@.

       /p:key[:value], /proverOpt:key[:value]
              Provide a prover-specific option.

              Set  the  platform  type and location.  ptype may be v11, v2, or cli1, and location
              should be the platform libraries directory.

              Use theorem prover p.  p may be a full path to a prover DLL, or it may  be  one  of
              the following standard provers:


                     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.

              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.

              Append (do not overwrite) the specified prover log file.

              Limit  the prover to n megabytes of virtual memory before forcing it to restart.  n
              defaults to 100.

              Set the time, in seconds, between closing the stream to the prover and killing  the
              prover process.  n defaults to 0.

              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.

              Restart the prover after each query.

              Limit the number of seconds spent trying to verify each procedure.

              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)
              Set Simplify's matching depth limit.

   Prover options (Z3)
              Use Z3's native array theory, as opposed to axioms.  Implies /monomorphize.

              Output a model in SMTLib2 format.

              Set  the  path  to  the  Z3  executable.   On  Debian  systems,  this  defaults  to

              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.

              Report multiple counterexamples for each error.

              Set an additional Z3 option.

              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 <>.

       This manual page is copyright © 2013, 2015-2016 Benjamin Barenblat and licensed under  the
       Apache License, Version 2.0.