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
|
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") {
}
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 bool Compile = true;
public bool ForceCompile = false;
protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {
Contract.Requires(name != null);
Contract.Requires(ps != null);
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 "compile": {
int compile = 0;
if (ps.GetNumericArgument(ref compile, 3)) {
Compile = compile == 1 || compile == 2;
ForceCompile = compile == 2;
}
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;
default:
break;
}
// not a Dafny-specific option, so defer to superclass
return base.ParseOption(name, ps);
}
protected 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)
/compile:<n> 0 - do not compile Dafny program
1 (default) - upon successful verification of the Dafny
program, compile Dafny program to C# program out.cs
2 - always attempt to compile Dafny program to C# program
out.cs, regardless of verification outcome
/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
");
}
}
}
|
