summaryrefslogtreecommitdiff
path: root/Source/Core/CommandLineOptions.ssc
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Core/CommandLineOptions.ssc')
-rw-r--r--Source/Core/CommandLineOptions.ssc13
1 files changed, 13 insertions, 0 deletions
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index 3645e7a3..07a21627 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -106,6 +106,7 @@ namespace Microsoft.Boogie
}
public string DafnyPrintFile = null;
+ public bool Compile = true;
public enum ProverWarnings { None, Stdout, Stderr }
public ProverWarnings PrintProverWarnings = ProverWarnings.None;
@@ -534,6 +535,15 @@ namespace Microsoft.Boogie
}
break;
+ case "-compile":
+ case "/compile": {
+ int compile = 0;
+ if (ps.GetNumericArgument(ref compile, 2)) {
+ Compile = compile == 1;
+ }
+ break;
+ }
+
case "-contracts":
case "/contracts":
case "-c":
@@ -1840,6 +1850,9 @@ namespace Microsoft.Boogie
/dprint:<file> : print Dafny program after parsing it
(use - as <file> to print to console)
+ /compile:<n> : 0 (default) - do not compile Dafny program
+ 1 - upon successful verification of the Dafny program,
+ compile Dafny program to C# program out.cs
---- Boogie options --------------------------------------------------------