1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
|
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;
using Bpl = Microsoft.Boogie;
namespace Microsoft.Dafny
{
public class DafnyOptions : Bpl.CommandLineOptions
{
public DafnyOptions()
: base("Dafny", "Dafny program verifier") {
}
public override string VersionNumber {
get {
return System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location).FileVersion;
}
}
private static DafnyOptions clo;
public static DafnyOptions O {
get { return clo; }
}
public static void Install(DafnyOptions options) {
Contract.Requires(options != null);
clo = options;
Bpl.CommandLineOptions.Install(options);
}
public bool DisallowSoundnessCheating = false;
public int Induction = 3;
public int InductionHeuristic = 6;
public string DafnyPrelude = null;
public string DafnyPrintFile = null;
public string DafnyPrintResolvedFile = null;
public bool Compile = true;
public bool ForceCompile = false;
public bool RunAfterCompile = false;
public bool SpillTargetCode = false;
public bool DisallowIncludes = false;
protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {
var args = ps.args; // convenient synonym
switch (name) {
case "dprelude":
if (ps.ConfirmArgumentCount(1)) {
DafnyPrelude = args[ps.i];
}
return true;
case "dprint":
if (ps.ConfirmArgumentCount(1)) {
DafnyPrintFile = args[ps.i];
}
return true;
case "rprint":
if (ps.ConfirmArgumentCount(1)) {
DafnyPrintResolvedFile = args[ps.i];
}
return true;
case "compile": {
int compile = 0;
if (ps.GetNumericArgument(ref compile, 4)) {
// convert option to two booleans
Compile = compile != 0;
ForceCompile = compile == 2;
RunAfterCompile = compile == 3;
}
return true;
}
case "spillTargetCode": {
int spill = 0;
if (ps.GetNumericArgument(ref spill, 2)) {
SpillTargetCode = spill != 0; // convert to a boolean
}
return true;
}
case "noCheating": {
int cheat = 0; // 0 is default, allows cheating
if (ps.GetNumericArgument(ref cheat, 2)) {
DisallowSoundnessCheating = cheat == 1;
}
return true;
}
case "induction":
ps.GetNumericArgument(ref Induction, 4);
return true;
case "inductionHeuristic":
ps.GetNumericArgument(ref InductionHeuristic, 7);
return true;
case "noIncludes":
DisallowIncludes = true;
return true;
default:
break;
}
// not a Dafny-specific option, so defer to superclass
return base.ParseOption(name, ps);
}
public override void ApplyDefaultOptions() {
base.ApplyDefaultOptions();
// expand macros in filenames, now that LogPrefix is fully determined
ExpandFilename(ref DafnyPrelude, LogPrefix, FileTimestamp);
ExpandFilename(ref DafnyPrintFile, LogPrefix, FileTimestamp);
}
public override void AttributeUsage() {
// TODO: provide attribute help here
}
public override void Usage() {
Console.WriteLine(@" ---- Dafny options ---------------------------------------------------------
Multiple .dfy files supplied on the command line are concatenated into one
Dafny program.
/dprelude:<file>
choose Dafny prelude file
/dprint:<file>
print Dafny program after parsing it
(use - as <file> to print to console)
/rprint:<file>
print Dafny program after resolving it
(use - as <file> to print to console)
/compile:<n> 0 - do not compile Dafny program
1 (default) - upon successful verification of the Dafny
program, compile Dafny program to .NET assembly
Program.exe (if the program has a Main method) or
Program.dll (othewise), where Program.dfy is the name
of the last .dfy file on the command line
2 - always attempt to compile Dafny program to C# program
out.cs, regardless of verification outcome
3 - if there is a Main method and there are no verification
errors, compiles program in memory (i.e., does not write
an output file) and runs it
/spillTargetCode:<n>
0 (default) - don't write the compiled Dafny program (but
still compile it, if /compile indicates to do so)
1 - write the compiled Dafny program as a .cs file
/noCheating:<n>
0 (default) - allow assume statements and free invariants
1 - treat all assumptions as asserts, and drop free.
/induction:<n>
0 - never do induction, not even when attributes request it
1 - only apply induction when attributes request it
2 - apply induction as requested (by attributes) and also
for heuristically chosen quantifiers
3 (default) - apply induction as requested, and for
heuristically chosen quantifiers and ghost methods
/inductionHeuristic:<n>
0 - least discriminating induction heuristic (that is, lean
toward applying induction more often)
1,2,3,4,5 - levels in between, ordered as follows as far as
how discriminating they are: 0 < 1 < 2 < (3,4) < 5 < 6
6 (default) - most discriminating
/noIncludes Ignore include directives
");
base.Usage(); // also print the Boogie options
}
}
}
|
