diff options
author | 2014-01-13 21:57:03 -0800 | |
---|---|---|
committer | 2014-01-13 21:57:03 -0800 | |
commit | d2b248851b9030697f71ead06e65a514805eb6d0 (patch) | |
tree | 63f15190942f5560774cd70c8c738f32f1b90873 /Source/Dafny | |
parent | 47637c8e97c4cb5f238de2f8d7f3870a869c372f (diff) | |
parent | 48d3c16cb2a20e3a0c761c590abe28adaa47fbfd (diff) |
Merge
Diffstat (limited to 'Source/Dafny')
-rw-r--r-- | Source/Dafny/DafnyOptions.cs | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index b69a9536..31fe6edd 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -38,6 +38,7 @@ namespace Microsoft.Dafny public string DafnyPrintResolvedFile = null;
public bool Compile = true;
public bool ForceCompile = false;
+ public bool RunAfterCompile = false;
public bool SpillTargetCode = false;
public bool DisallowIncludes = false;
@@ -65,10 +66,11 @@ namespace Microsoft.Dafny case "compile": {
int compile = 0;
- if (ps.GetNumericArgument(ref compile, 3)) {
+ if (ps.GetNumericArgument(ref compile, 4)) {
// convert option to two booleans
- Compile = compile == 1 || compile == 2;
+ Compile = compile != 0;
ForceCompile = compile == 2;
+ RunAfterCompile = compile == 3;
}
return true;
}
@@ -136,9 +138,15 @@ namespace Microsoft.Dafny (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
+ 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)
|