Add support for the /verifySeparately flag in Boogie and change most tests to use it.

9 files changed, 109 insertions, 79 deletions

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index a6256580..10c7e90a 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -97,7 +97,22 @@ namespace Microsoft.Dafny
     static ExitValue ProcessFiles(List<string/*!*/>/*!*/ fileNames)

     {

       Contract.Requires(cce.NonNullElements(fileNames));

+

       ExitValue exitValue = ExitValue.VERIFIED;

+      if (CommandLineOptions.Clo.VerifySeparately && 1 < fileNames.Count)

+      {

+        foreach (var f in fileNames)

+        {

+          Console.WriteLine("\n-------------------- {0} --------------------", f);

+          var ev = ProcessFiles(new List<string> { f });

+          if (exitValue != ev && ev != ExitValue.VERIFIED)

+          {

+            exitValue = ev;

+          }

+        }

+        return exitValue;

+      }

+      

       using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count-1])) {

         Dafny.Program dafnyProgram;

         string programName = fileNames.Count == 1 ? fileNames[0] : "the program";

diff --git a/Test/VSComp2010/Answer b/Test/VSComp2010/Answer
index 9a083fa3..ff491aa5 100644
--- a/Test/VSComp2010/Answer
+++ b/Test/VSComp2010/Answer
@@ -1,20 +1,20 @@
-

+
 -------------------- Problem1-SumMax.dfy --------------------

 

 Dafny program verifier finished with 4 verified, 0 errors

-

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

 

 Dafny program verifier finished with 7 verified, 0 errors

-

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

 

 Dafny program verifier finished with 7 verified, 0 errors

-

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

 

 Dafny program verifier finished with 9 verified, 0 errors

-

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

 

 Dafny program verifier finished with 21 verified, 0 errors

diff --git a/Test/VSComp2010/runtest.bat b/Test/VSComp2010/runtest.bat
index 4e6d170b..2cfcdafb 100644
--- a/Test/VSComp2010/runtest.bat
+++ b/Test/VSComp2010/runtest.bat
@@ -4,10 +4,12 @@ setlocal
 set BINARIES=..\..\Binaries

 set DAFNY_EXE=%BINARIES%\Dafny.exe

 

-for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy

-            Problem3-FindZero.dfy Problem4-Queens.dfy

-            Problem5-DoubleEndedQueue.dfy) do (

-  echo.

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

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

-)

+%DAFNY_EXE% /compile:0 /verifySeparately %* Problem1-SumMax.dfy Problem2-Invert.dfy Problem3-FindZero.dfy Problem4-Queens.dfy Problem5-DoubleEndedQueue.dfy

+

+rem for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy

+rem             Problem3-FindZero.dfy Problem4-Queens.dfy

+rem             Problem5-DoubleEndedQueue.dfy) do (

+rem   echo.

+rem   echo -------------------- %%f --------------------

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

+rem )

diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat
index bbb9e3d7..f950cf2a 100644
--- a/Test/VSI-Benchmarks/runtest.bat
+++ b/Test/VSI-Benchmarks/runtest.bat
@@ -4,8 +4,10 @@ setlocal
 set BINARIES=..\..\Binaries

 set DAFNY_EXE=%BINARIES%\Dafny.exe

 

-for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do (

-  echo.

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

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

-)

+%DAFNY_EXE% /compile:0 /verifySeparately %* b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy

+

+rem for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do (

+rem   echo.

+rem   echo -------------------- %%f --------------------

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

+rem )

diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
index 5a43205f..f02a7965 100644
--- a/Test/dafny1/runtest.bat
+++ b/Test/dafny1/runtest.bat
@@ -4,21 +4,23 @@ setlocal
 set BINARIES=..\..\Binaries

 set DAFNY_EXE=%BINARIES%\Dafny.exe

 

-for %%f in (Queue.dfy PriorityQueue.dfy

-            ExtensibleArray.dfy ExtensibleArrayAuto.dfy

-            BinaryTree.dfy

-            UnboundedStack.dfy

-            SeparationLogicList.dfy

-            ListCopy.dfy ListReverse.dfy ListContents.dfy

-            MatrixFun.dfy pow2.dfy

-            SchorrWaite.dfy SchorrWaite-stages.dfy

-            Cubes.dfy SumOfCubes.dfy FindZero.dfy

-            TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy

-            Induction.dfy Rippling.dfy MoreInduction.dfy

-            Celebrity.dfy BDD.dfy

-            UltraFilter.dfy

-            ) do (

-  echo.

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

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

-)

+%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /verifySeparately %* Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy ExtensibleArrayAuto.dfy BinaryTree.dfy UnboundedStack.dfy SeparationLogicList.dfy ListCopy.dfy ListReverse.dfy ListContents.dfy MatrixFun.dfy pow2.dfy SchorrWaite.dfy SchorrWaite-stages.dfy Cubes.dfy SumOfCubes.dfy FindZero.dfy TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy Induction.dfy Rippling.dfy MoreInduction.dfy Celebrity.dfy BDD.dfy UltraFilter.dfy

+

+rem for %%f in (Queue.dfy PriorityQueue.dfy

+rem             ExtensibleArray.dfy ExtensibleArrayAuto.dfy

+rem             BinaryTree.dfy

+rem             UnboundedStack.dfy

+rem             SeparationLogicList.dfy

+rem             ListCopy.dfy ListReverse.dfy ListContents.dfy

+rem             MatrixFun.dfy pow2.dfy

+rem             SchorrWaite.dfy SchorrWaite-stages.dfy

+rem             Cubes.dfy SumOfCubes.dfy FindZero.dfy

+rem             TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy

+rem             Induction.dfy Rippling.dfy MoreInduction.dfy

+rem             Celebrity.dfy BDD.dfy

+rem             UltraFilter.dfy

+rem             ) do (

+rem   echo.

+rem   echo -------------------- %%f --------------------

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

+rem )

diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat
index 72706d8f..d038acce 100644
--- a/Test/dafny2/runtest.bat
+++ b/Test/dafny2/runtest.bat
@@ -5,20 +5,23 @@ set BINARIES=..\..\Binaries
 set DAFNY_EXE=%BINARIES%\Dafny.exe

 

 REM soon again:    SnapshotableTrees.dfy

-for %%f in (

-    Classics.dfy

-    TreeBarrier.dfy

-    COST-verif-comp-2011-1-MaxArray.dfy

-    COST-verif-comp-2011-2-MaxTree-class.dfy

-    COST-verif-comp-2011-2-MaxTree-datatype.dfy

-    COST-verif-comp-2011-3-TwoDuplicates.dfy

-    COST-verif-comp-2011-4-FloydCycleDetect.dfy

-    StoreAndRetrieve.dfy

-    Intervals.dfy TreeFill.dfy TuringFactorial.dfy

-    MajorityVote.dfy SegmentSum.dfy

-    MonotonicHeapstate.dfy Calculations.dfy

-  ) do (

-  echo.

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

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

-)

+

+%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /verifySeparately %* Classics.dfy TreeBarrier.dfy COST-verif-comp-2011-1-MaxArray.dfy COST-verif-comp-2011-2-MaxTree-class.dfy COST-verif-comp-2011-2-MaxTree-datatype.dfy COST-verif-comp-2011-3-TwoDuplicates.dfy COST-verif-comp-2011-4-FloydCycleDetect.dfy StoreAndRetrieve.dfy Intervals.dfy TreeFill.dfy TuringFactorial.dfy MajorityVote.dfy SegmentSum.dfy MonotonicHeapstate.dfy Calculations.dfy

+

+rem for %%f in (

+rem     Classics.dfy

+rem     TreeBarrier.dfy

+rem     COST-verif-comp-2011-1-MaxArray.dfy

+rem     COST-verif-comp-2011-2-MaxTree-class.dfy

+rem     COST-verif-comp-2011-2-MaxTree-datatype.dfy

+rem     COST-verif-comp-2011-3-TwoDuplicates.dfy

+rem     COST-verif-comp-2011-4-FloydCycleDetect.dfy

+rem     StoreAndRetrieve.dfy

+rem     Intervals.dfy TreeFill.dfy TuringFactorial.dfy

+rem     MajorityVote.dfy SegmentSum.dfy

+rem     MonotonicHeapstate.dfy Calculations.dfy

+rem   ) do (

+rem   echo.

+rem   echo -------------------- %%f --------------------

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

+rem )

diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat
index 9bce80c5..40992f28 100644
--- a/Test/dafny3/runtest.bat
+++ b/Test/dafny3/runtest.bat
@@ -4,14 +4,16 @@ setlocal
 set BINARIES=..\..\Binaries

 set DAFNY_EXE=%BINARIES%\Dafny.exe

 

-for %%f in (

-  Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy

-  SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy

-  InductionVsCoinduction.dfy Zip.dfy SetIterations.dfy

-  Paulson.dfy Filter.dfy WideTrees.dfy InfiniteTrees.dfy

-  OpaqueTrees.dfy

-) do (

-  echo.

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

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

-)

+%DAFNY_EXE% /compile:0 /verifySeparately %* Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy InductionVsCoinduction.dfy Zip.dfy SetIterations.dfy Paulson.dfy Filter.dfy WideTrees.dfy InfiniteTrees.dfy OpaqueTrees.dfy

+

+rem for %%f in (

+rem   Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy

+rem   SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy

+rem   InductionVsCoinduction.dfy Zip.dfy SetIterations.dfy

+rem   Paulson.dfy Filter.dfy WideTrees.dfy InfiniteTrees.dfy

+rem   OpaqueTrees.dfy

+rem ) do (

+rem   echo.

+rem   echo -------------------- %%f --------------------

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

+rem )

diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat
index 63fd2001..d7f31c3b 100644
--- a/Test/vacid0/runtest.bat
+++ b/Test/vacid0/runtest.bat
@@ -4,8 +4,10 @@ setlocal
 set BINARIES=..\..\Binaries

 set DAFNY_EXE=%BINARIES%\Dafny.exe

 

-for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do (

-  echo.

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

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

-)

+%DAFNY_EXE% /compile:0 /verifySeparately %* LazyInitArray.dfy SparseArray.dfy Composite.dfy

+

+rem for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do (

+rem   echo.

+rem   echo -------------------- %%f --------------------

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

+rem )

diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat
index ecccd929..5d7953cc 100644
--- a/Test/vstte2012/runtest.bat
+++ b/Test/vstte2012/runtest.bat
@@ -4,14 +4,16 @@ setlocal
 set BINARIES=..\..\Binaries

 set DAFNY_EXE=%BINARIES%\Dafny.exe

 

-for %%f in (

-    Two-Way-Sort.dfy

-    Combinators.dfy

-    RingBuffer.dfy RingBufferAuto.dfy

-    Tree.dfy

-    BreadthFirstSearch.dfy

-  ) do (

-  echo.

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

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

-)

+%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /verifySeparately %* Two-Way-Sort.dfy Combinators.dfy RingBuffer.dfy RingBufferAuto.dfy Tree.dfy BreadthFirstSearch.dfy

+

+rem for %%f in (

+rem     Two-Way-Sort.dfy

+rem     Combinators.dfy

+rem     RingBuffer.dfy RingBufferAuto.dfy

+rem     Tree.dfy

+rem     BreadthFirstSearch.dfy

+rem   ) do (

+rem   echo.

+rem   echo -------------------- %%f --------------------

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

+rem )