diff options
Diffstat (limited to 'Source/Dafny/DafnyOptions.cs')
| -rw-r--r-- | Source/Dafny/DafnyOptions.cs | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index eb01ac12..34fa0487 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -29,6 +29,7 @@ namespace Microsoft.Dafny 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 SpillTargetCode = false;
@@ -49,6 +50,12 @@ namespace Microsoft.Dafny }
return true;
+ case "rprint":
+ if (ps.ConfirmArgumentCount(1)) {
+ DafnyPrintResolvedFile = args[ps.i];
+ }
+ return true;
+
case "compile": {
int compile = 0;
if (ps.GetNumericArgument(ref compile, 3)) {
@@ -113,6 +120,9 @@ namespace Microsoft.Dafny /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 C# program out.cs
|