Dafny: call C# compiler directly from inside Dafny, and optionally produce a .cs file with the new /spillTargetCode switch

1 files changed, 14 insertions, 0 deletions

diff --git a/Dafny/DafnyOptions.cs b/Dafny/DafnyOptions.cs
index 745d50ef..4a1388d9 100644
--- a/Dafny/DafnyOptions.cs
+++ b/Dafny/DafnyOptions.cs
@@ -31,6 +31,7 @@ namespace Microsoft.Dafny
     public string DafnyPrintFile = null;

     public bool Compile = true;

     public bool ForceCompile = false;

+    public bool SpillTargetCode = false;

 

     protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {

       var args = ps.args;  // convenient synonym

@@ -51,12 +52,21 @@ namespace Microsoft.Dafny
         case "compile": {

             int compile = 0;

             if (ps.GetNumericArgument(ref compile, 3)) {

+              // convert option to two booleans

               Compile = compile == 1 || compile == 2;

               ForceCompile = compile == 2;

             }

             return true;

           }

 

+        case "spillTargetCode": {

+            int spill = 0;

+            if (ps.GetNumericArgument(ref spill, 2)) {

+              SpillTargetCode = spill != 0;  // convert to a boolean

+            }

+            return true;

+          }

+

         case "noCheating": {

             int cheat = 0; // 0 is default, allows cheating

             if (ps.GetNumericArgument(ref cheat, 2)) {

@@ -108,6 +118,10 @@ namespace Microsoft.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

+  /spillTargetCode:<n>

+                0 (default) - don't write the compiled Dafny program (but

+                    still compile it, if /compile indicates to do so)

+                1 - write the compiled Dafny program as a .cs file

   /noCheating:<n>

                 0 (default) - allow assume statements and free invariants

                 1 - treat all assumptions as asserts, and drop free.