Merge

8 files changed, 26 insertions, 63 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/inline/Answer b/Test/inline/Answer
index 2c29ab0b..d7e7edbe 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -32,7 +32,7 @@ procedure {:inline 1} incdec(x: int, y: int) returns (z: int);
 

 

 

-implementation incdec(x: int, y: int) returns (z: int)

+implementation {:inline 1} incdec(x: int, y: int) returns (z: int)

 {

 

   anon0:

@@ -49,7 +49,7 @@ procedure {:inline 1} inc(x: int, i: int) returns (y: int);
 

 

 

-implementation inc(x: int, i: int) returns (y: int)

+implementation {:inline 1} inc(x: int, i: int) returns (y: int)

 {

 

   anon0:

@@ -65,7 +65,7 @@ procedure {:inline 1} dec(x: int, i: int) returns (y: int);
 

 

 

-implementation dec(x: int, i: int) returns (y: int)

+implementation {:inline 1} dec(x: int, i: int) returns (y: int)

 {

 

   anon0:

@@ -160,7 +160,7 @@ procedure {:inline 1} incdec(x: int, y: int) returns (z: int);
   ensures z == x + 1 - y;

 

 

-implementation incdec(x: int, y: int) returns (z: int)

+implementation {:inline 1} incdec(x: int, y: int) returns (z: int)

 {

   var inline$dec$0$x: int;

   var inline$dec$0$i: int;

@@ -220,7 +220,7 @@ procedure {:inline 1} increase(i: int) returns (k: int);
 

 

 

-implementation increase(i: int) returns (k: int)

+implementation {:inline 1} increase(i: int) returns (k: int)

 {

   var j: int;

 

@@ -298,7 +298,7 @@ procedure {:inline 3} recursive(x: int) returns (y: int);
 

 

 

-implementation recursive(x: int) returns (y: int)

+implementation {:inline 3} recursive(x: int) returns (y: int)

 {

   var k: int;

 

@@ -421,7 +421,7 @@ after inlining procedure calls
 procedure {:inline 3} recursive(x: int) returns (y: int);

 

 

-implementation recursive(x: int) returns (y: int)

+implementation {:inline 3} recursive(x: int) returns (y: int)

 {

   var k: int;

   var inline$recursive$0$k: int;

@@ -560,7 +560,7 @@ procedure {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, fo
 

 

 

-implementation find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)

+implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)

 {

   var i: int;

   var b: bool;

@@ -606,7 +606,7 @@ procedure {:inline 3} check(A: [int]int, i: int, c: int) returns (ret: bool);
 

 

 

-implementation check(A: [int]int, i: int, c: int) returns (ret: bool)

+implementation {:inline 3} check(A: [int]int, i: int, c: int) returns (ret: bool)

 {

 

   anon0:

@@ -746,7 +746,7 @@ after inlining procedure calls
 procedure {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool);

 

 

-implementation find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)

+implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)

 {

   var i: int;

   var b: bool;

@@ -866,7 +866,7 @@ procedure {:inline 2} foo();
 

 

 

-implementation foo()

+implementation {:inline 2} foo()

 {

 

   anon0:

@@ -882,7 +882,7 @@ procedure {:inline 2} foo1();
 

 

 

-implementation foo1()

+implementation {:inline 2} foo1()

 {

 

   anon0:

@@ -898,7 +898,7 @@ procedure {:inline 2} foo2();
 

 

 

-implementation foo2()

+implementation {:inline 2} foo2()

 {

 

   anon0:

@@ -914,7 +914,7 @@ procedure {:inline 2} foo3();
 

 

 

-implementation foo3()

+implementation {:inline 2} foo3()

 {

 

   anon0:

@@ -947,7 +947,7 @@ procedure {:inline 2} foo();
   modifies x;

 

 

-implementation foo()

+implementation {:inline 2} foo()

 {

   var inline$foo$0$x: int;

   var inline$foo$1$x: int;

@@ -992,7 +992,7 @@ procedure {:inline 2} foo1();
   modifies x;

 

 

-implementation foo1()

+implementation {:inline 2} foo1()

 {

   var inline$foo2$0$x: int;

   var inline$foo3$0$x: int;

@@ -1097,7 +1097,7 @@ procedure {:inline 2} foo2();
   modifies x;

 

 

-implementation foo2()

+implementation {:inline 2} foo2()

 {

   var inline$foo3$0$x: int;

   var inline$foo1$0$x: int;

@@ -1202,7 +1202,7 @@ procedure {:inline 2} foo3();
   modifies x;

 

 

-implementation foo3()

+implementation {:inline 2} foo3()

 {

   var inline$foo1$0$x: int;

   var inline$foo2$0$x: int;

@@ -1532,7 +1532,7 @@ procedure {:inline 1} foo();
 

 

 

-implementation foo()

+implementation {:inline 1} foo()

 {

 

   anon0:

@@ -1605,7 +1605,7 @@ procedure {:inline 1} foo();
   modifies g;

 

 

-implementation foo()

+implementation {:inline 1} foo()

 {

   var inline$bar$0$g: int;

 

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

 )