From c5b2aec063fc1f3d5e61ff1b14983c5e4ba7c2ea Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Tue, 1 Jul 2014 00:55:31 +0200
Subject: Added support for verifying Dafny program snapshots from the
 command-line.

---
 Source/DafnyDriver/DafnyDriver.cs | 20 +++++++++++++++++---
 1 file changed, 17 insertions(+), 3 deletions(-)

(limited to 'Source/DafnyDriver')

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 8f5b5300..01ee269e 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -99,7 +99,7 @@ namespace Microsoft.Dafny
     }
 
 
-    static ExitValue ProcessFiles(List<string/*!*/>/*!*/ fileNames)
+    static ExitValue ProcessFiles(List<string/*!*/>/*!*/ fileNames, bool lookForSnapshots = true)
     {
       Contract.Requires(cce.NonNullElements(fileNames));
 
@@ -110,7 +110,21 @@ namespace Microsoft.Dafny
         {
           Console.WriteLine();
           Console.WriteLine("-------------------- {0} --------------------", f);
-          var ev = ProcessFiles(new List<string> { f });
+          var ev = ProcessFiles(new List<string> { f }, lookForSnapshots);
+          if (exitValue != ev && ev != ExitValue.VERIFIED)
+          {
+            exitValue = ev;
+          }
+        }
+        return exitValue;
+      }
+
+      if (0 < CommandLineOptions.Clo.VerifySnapshots && lookForSnapshots)
+      {
+        var snapshotsByVersion = ExecutionEngine.LookForSnapshots(fileNames);
+        foreach (var s in snapshotsByVersion)
+        {
+          var ev = ProcessFiles(new List<string>(s), false);
           if (exitValue != ev && ev != ExitValue.VERIFIED)
           {
             exitValue = ev;
@@ -213,7 +227,7 @@ namespace Microsoft.Dafny
           ExecutionEngine.CollectModSets(program);
           ExecutionEngine.CoalesceBlocks(program);
           ExecutionEngine.Inline(program);
-          return ExecutionEngine.InferAndVerify(program, stats);
+          return ExecutionEngine.InferAndVerify(program, stats, 1 < Dafny.DafnyOptions.Clo.VerifySnapshots ? "main_program_id" : null);
 
         default:
           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected outcome
-- 
cgit v1.2.3