Provided by: dafny_2.3.0+dfsg-0.1_all 
NAME
dafny - compiler for the Dafny programming language
SYNOPSIS
dafny [options] file.dfy ...
DESCRIPTION
dafny is a compiler for Microsoft Research's Dafny programming language, an imperative
language with built-in specification constructs. The integrated static analyzer can
verify functional correctness as part of the compilation process.
OPTIONS
dafny accepts a number of different types of options.
File macros
A number of dafny 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.
Dafny options
Multiple .dfy files supplied on the command line are concatenated into one Dafny program.
/allowGlobals
Allow the implicit class _default to contain fields, instance functions, and
instance methods. These class members are declared at module scope, outside of
explicit classes. This command-line option is provided to simplify a a transition
from the behavior in the language prior to version 1.9.3, from which point onward
all functions and methods declared at the module scope are implicitly static and
field declarations are not allowed at the module scope.
/autoReqPrint:file
Print requirements automatically generated by autoReq to the specified file.
/compile:n
Enable or disable compilation. Accepted values for n are:
0 Do not compile.
1 (default) Compile Dafny to CLI assembly. The output file name shares the
base name of the last .dfy file on the command line. If the program has a
Main method, the output will have the extension .exe; otherwise, it will be
a .dll.
/dafnycc
Disable features not supported by DafnyCC.
/dafnyVerify:n
Control how far compilation proceeds. Accepted values for n are:
0 Stop after typechecking.
1 Typecheck, verify, and compile.
/dprelude:file
Choose Dafny prelude file.
/dprint:file
Print Dafny program to the specified file after parsing. Specify /dprint:- to
print to standard output.
/induction:n
Control when Dafny performs induction. Accepted values for n are:
0 Never do induction, not even when attributes request it.
1 Apply induction only when attributes request it.
2 Apply induction as requested by attributes and also for heuristically chosen
quantifiers.
3 (default) Apply induction as requested by attributes, for heuristically
chosen quantifiers, and for ghost methods.
/inductionHeuristic:n
Control how discriminating the induction heuristic is. /inductionHeuristic:0 is
the least discriminating (that is, it leans toward applying induction most often);
increasing n up to 6, the default, increases dafny's reluctance to apply induction.
/noAutoReq
Ignore autoReq attributes.
/noCheating:n
Control how strict dafny is about unproven constructs. Accepted values for n are:
0 (default) Allow assume statements and free invariants.
1 Treat all assumptions as assertions, and drop free.
/noIncludes
Ignore include directives.
/noNLarith
Reduce Z3's knowledge of nonlinear arithmetic (multiplication and division). This
results in more manual work but also tends to produce more predictable behavior.
/printMode:mode
Control printing. Accepted values for mode are:
Everything
(default) Print everything.
NoIncludes
Disable printing of "{:verify false} methods incorporated via the include
mechanism, as well as datatypes and fields included from other files.
NoGhost
Like NoIncludes, but also disable printing of functions ghost methods, and
proof statements in implementation methods.
/rprint:file
Print Dafny program to the specified file after resolving it. Specify /rprint:- to
print to standard output.
/spillTargetCode:n
Control whether or not dafny emits intermediate C# code. Accepted values for n
are:
0 (default) Don't save intermediate C# code.
1 Save intermediate C# code as a .cs 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.
/pretty:n
Control pretty-printing of Boogie code. Accepted values for n are:
0 Print each Boogie statement on one line.
1 (default) Pretty-print with some line breaks. This is slower but easier to
read.
/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.
/printUnstructured
With /print, desugar all structured statements.
/printWithUniqueIds
Print augmented information that uniquely identifies variables.
/proc:p
Limit which procedures to check.
/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
Control verification result caching. Accepted values for n are:
0 (default) Do not use any verification result caching.
1 Verify several program snapshots (named filename.v0.bpl to filename.vN.bpl)
using basic verification result caching.
2 Use more advanced verification result caching.
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, dafny 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 dafny 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 dafny 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 (CVC4)
/cvc4exe:path
Set the path to the CVC4 executable.
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)
COPYRIGHT
Dafny 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 Benjamin Barenblat and licensed under the
Apache License, Version 2.0.