forked from dafny-lang/dafny
-
Notifications
You must be signed in to change notification settings - Fork 0
/
DafnyCommands.cs
100 lines (89 loc) · 3.57 KB
/
DafnyCommands.cs
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
using System.Collections.Generic;
using System.CommandLine;
using System.IO;
using System.Linq;
namespace Microsoft.Dafny;
public static class DafnyCommands {
public static Argument<FileInfo> FileArgument { get; }
public static Argument<List<FileInfo>> FilesArgument { get; }
static DafnyCommands() {
FileArgument = new Argument<FileInfo>("file", "Dafny input file or Dafny project file");
FilesArgument = new("file", r => {
return r.Tokens.Where(t => !string.IsNullOrEmpty(t.Value)).Select(t => new FileInfo(t.Value)).ToList();
}, false, "Dafny input files and/or a Dafny project file");
}
public static IEnumerable<Option> FormatOptions => new Option[] {
CommonOptionBag.Check,
CommonOptionBag.FormatPrint,
}.Concat(ParserOptions);
public static IReadOnlyList<Option> VerificationOptions = new Option[] {
CommonOptionBag.RelaxDefiniteAssignment,
BoogieOptionBag.VerificationTimeLimit,
CommonOptionBag.VerifyIncludedFiles,
CommonOptionBag.ManualLemmaInduction,
BoogieOptionBag.SolverPath,
CommonOptionBag.DisableNonLinearArithmetic,
BoogieOptionBag.IsolateAssertions,
BoogieOptionBag.BoogieArguments,
CommonOptionBag.VerificationLogFormat,
BoogieOptionBag.SolverResourceLimit,
BoogieOptionBag.SolverOption,
BoogieOptionBag.SolverOptionHelp,
BoogieOptionBag.SolverPlugin,
BoogieOptionBag.SolverLog,
CommonOptionBag.JsonDiagnostics,
BoogieOptionBag.VerificationErrorLimit,
CommonOptionBag.DefaultFunctionOpacity,
CommonOptionBag.WarnContradictoryAssumptions,
CommonOptionBag.WarnRedundantAssumptions,
CommonOptionBag.NoTimeStampForCoverageReport,
CommonOptionBag.VerificationCoverageReport
}.ToList();
public static IReadOnlyList<Option> TranslationOptions = new Option[] {
BoogieOptionBag.NoVerify,
CommonOptionBag.EnforceDeterminism,
CommonOptionBag.OptimizeErasableDatatypeWrapper,
CommonOptionBag.TestAssumptions,
DeveloperOptionBag.Bootstrapping,
CommonOptionBag.AddCompileSuffix,
CommonOptionBag.SystemModule
}.Concat(VerificationOptions).ToList();
public static IReadOnlyList<Option> ExecutionOptions = new Option[] {
CommonOptionBag.Target,
CommonOptionBag.SpillTranslation,
CommonOptionBag.InternalIncludeRuntimeOptionForExecution,
CommonOptionBag.ExecutionCoverageReport
}.Concat(TranslationOptions).ToList();
public static IReadOnlyList<Option> ConsoleOutputOptions = new List<Option>(new Option[] {
DafnyConsolePrinter.ShowSnippets,
DeveloperOptionBag.Print,
DeveloperOptionBag.ResolvedPrint,
DeveloperOptionBag.BoogiePrint,
Printer.PrintMode,
CommonOptionBag.WarningAsErrors,
});
public static IReadOnlyList<Option> ParserOptions = new List<Option>(new Option[] {
CommonOptionBag.StdIn,
CommonOptionBag.Verbose,
BoogieOptionBag.Cores,
CommonOptionBag.Libraries,
CommonOptionBag.WarnDeprecation,
CommonOptionBag.PluginOption,
CommonOptionBag.Prelude,
Function.FunctionSyntaxOption,
CommonOptionBag.QuantifierSyntax,
CommonOptionBag.UnicodeCharacters,
CommonOptionBag.UseBaseFileName,
CommonOptionBag.GeneralTraits,
CommonOptionBag.TypeSystemRefresh,
CommonOptionBag.TypeInferenceDebug,
CommonOptionBag.NewTypeInferenceDebug,
CommonOptionBag.ReadsClausesOnMethods,
CommonOptionBag.UseStandardLibraries
});
public static IReadOnlyList<Option> ResolverOptions = new List<Option>(new Option[] {
CommonOptionBag.WarnShadowing,
CommonOptionBag.WarnMissingConstructorParenthesis,
PrintStmt.TrackPrintEffectsOption,
}).Concat(ParserOptions).ToList();
}