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

7 files changed, 6 insertions, 43 deletions

diff --git a/Test/VSComp2010/Answer b/Test/VSComp2010/Answer
index dc523fdf..9a083fa3 100644
--- a/Test/VSComp2010/Answer
+++ b/Test/VSComp2010/Answer
@@ -2,24 +2,19 @@
 -------------------- Problem1-SumMax.dfy --------------------

 

 Dafny program verifier finished with 4 verified, 0 errors

-Compiled program written to out.cs

 

 -------------------- Problem2-Invert.dfy --------------------

 

 Dafny program verifier finished with 7 verified, 0 errors

-Compiled program written to out.cs

 

 -------------------- Problem3-FindZero.dfy --------------------

 

 Dafny program verifier finished with 7 verified, 0 errors

-Compiled program written to out.cs

 

 -------------------- Problem4-Queens.dfy --------------------

 

 Dafny program verifier finished with 9 verified, 0 errors

-Compiled program written to out.cs

 

 -------------------- Problem5-DoubleEndedQueue.dfy --------------------

 

 Dafny program verifier finished with 21 verified, 0 errors

-Compiled program written to out.cs

diff --git a/Test/VSComp2010/runtest.bat b/Test/VSComp2010/runtest.bat
index e16eda13..9535d677 100644
--- a/Test/VSComp2010/runtest.bat
+++ b/Test/VSComp2010/runtest.bat
@@ -11,7 +11,5 @@ for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy
             Problem5-DoubleEndedQueue.dfy) do (

   echo.

   echo -------------------- %%f --------------------

-  %DAFNY_EXE% %* %%f

-

-  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs

+  %DAFNY_EXE% /compile:0 %* %%f

 )

diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat
index a733a1c0..611f9251 100644
--- a/Test/VSI-Benchmarks/runtest.bat
+++ b/Test/VSI-Benchmarks/runtest.bat
@@ -9,11 +9,5 @@ set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
 for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do (

   echo.

   echo -------------------- %%f --------------------

-

-  REM The following line will just run the verifier

-  IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 %* %%f

-

-  REM Alternatively, the following lines also produce C# code and compile it

-  IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f

-  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs

+  %DAFNY_EXE% /compile:0 %* %%f

 )

diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
index 15bd28a1..524765cf 100644
--- a/Test/dafny1/runtest.bat
+++ b/Test/dafny1/runtest.bat
@@ -26,11 +26,5 @@ for %%f in (Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy
             UltraFilter.dfy) do (

   echo.

   echo -------------------- %%f --------------------

-

-  REM The following line will just run the verifier

-  IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f

-

-  REM Alternatively, the following lines also produce C# code and compile it

-  IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f

-  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs

+  %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f

 )

diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat
index 50b4ca18..6c723ea5 100644
--- a/Test/dafny2/runtest.bat
+++ b/Test/dafny2/runtest.bat
@@ -16,11 +16,5 @@ for %%f in (
   ) do (

   echo.

   echo -------------------- %%f --------------------

-

-  REM The following line will just run the verifier

-  IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f

-

-  REM Alternatively, the following lines also produce C# code and compile it

-  IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f

-  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs

+  %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f

 )

diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat
index 32c6a984..efe7b3d5 100644
--- a/Test/vacid0/runtest.bat
+++ b/Test/vacid0/runtest.bat
@@ -9,11 +9,5 @@ set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
 for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do (

   echo.

   echo -------------------- %%f --------------------

-

-  REM The following line will just run the verifier

-  IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 %* %%f

-

-  REM Alternatively, the following lines also produce C# code and compile it

-  IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f

-  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs

+  %DAFNY_EXE% /compile:0 %* %%f

 )

diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat
index 07b5859e..5145cb56 100644
--- a/Test/vstte2012/runtest.bat
+++ b/Test/vstte2012/runtest.bat
@@ -14,11 +14,5 @@ for %%f in (
   ) do (

   echo.

   echo -------------------- %%f --------------------

-

-  REM The following line will just run the verifier

-  IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f

-

-  REM Alternatively, the following lines also produce C# code and compile it

-  IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f

-  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs

+  %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f

 )