From 42d8a89ea406dc001dfd83af2e2d66f5ed813cc7 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Wed, 18 Dec 2013 11:14:19 +0100
Subject: Add support for the /verifySeparately flag in Boogie and change most
 tests to use it.

---
 Source/DafnyDriver/DafnyDriver.cs | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'Source/DafnyDriver')

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";
-- 
cgit v1.2.3