Worked on the more advanced verification result caching.

6 files changed, 46 insertions, 8 deletions

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index ea21f12b..8c0f3235 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -182,18 +182,19 @@ namespace DafnyLanguage
 

     class DafnyErrorInformationFactory : ErrorInformationFactory

     {

-      public override ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId, string category = null)

+      public override ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId, string originalRequestId, string category = null)

       {

-        return new DafnyErrorInformation(tok, msg, requestId, category);

+        return new DafnyErrorInformation(tok, msg, requestId, originalRequestId, category);

       }

     }

 

     class DafnyErrorInformation : ErrorInformation

     {

-      public DafnyErrorInformation(IToken tok, string msg, string requestId, string category = null)

+      public DafnyErrorInformation(IToken tok, string msg, string requestId, string originalRequestId, string category = null)

         : base(tok, msg)

       {

         RequestId = requestId;

+        OriginalRequestId = originalRequestId;

         Category = category;

         AddNestingsAsAux(tok);

       }

diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index 3da47538..360ee209 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -340,13 +340,14 @@ namespace DafnyLanguage
           if (!_disposed)

           {

             errorInfo.BoogieErrorCode = null;

-            if (errorInfo.RequestId != null && RequestIdToSnapshot.ContainsKey(errorInfo.RequestId))

+            var recycled = errorInfo.OriginalRequestId != requestId ? " (recycled)" : "";

+            if (errorInfo.OriginalRequestId != null && RequestIdToSnapshot.ContainsKey(errorInfo.OriginalRequestId))

             {

-              var s = RequestIdToSnapshot[errorInfo.RequestId];

-              errorListHolder.AddError(new DafnyError(errorInfo.Tok.filename, errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.FullMsg, s, errorInfo.Model.ToString(), System.IO.Path.GetFullPath(_document.FilePath) == errorInfo.Tok.filename), errorInfo.ImplementationName, requestId);

+              var s = RequestIdToSnapshot[errorInfo.OriginalRequestId];

+              errorListHolder.AddError(new DafnyError(errorInfo.Tok.filename, errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.FullMsg + recycled, s, errorInfo.Model.ToString(), System.IO.Path.GetFullPath(_document.FilePath) == errorInfo.Tok.filename), errorInfo.ImplementationName, errorInfo.OriginalRequestId);

               foreach (var aux in errorInfo.Aux)

               {

-                errorListHolder.AddError(new DafnyError(aux.Tok.filename, aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.FullMsg, s, null, System.IO.Path.GetFullPath(_document.FilePath) == aux.Tok.filename), errorInfo.ImplementationName, requestId);

+                errorListHolder.AddError(new DafnyError(aux.Tok.filename, aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.FullMsg, s, null, System.IO.Path.GetFullPath(_document.FilePath) == aux.Tok.filename), errorInfo.ImplementationName, errorInfo.OriginalRequestId);

               }

             }

           }

diff --git a/Test/dafny0/snapshots/Snapshots3.v0.dfy b/Test/dafny0/snapshots/Snapshots3.v0.dfy
new file mode 100644
index 00000000..72607412
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots3.v0.dfy
@@ -0,0 +1,11 @@
+method M()

+{

+  if (*)

+  {

+    

+  }

+  else

+  {

+    assert 0 != 0;  // error

+  }

+}

diff --git a/Test/dafny0/snapshots/Snapshots3.v1.dfy b/Test/dafny0/snapshots/Snapshots3.v1.dfy
new file mode 100644
index 00000000..3b186318
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots3.v1.dfy
@@ -0,0 +1,11 @@
+method M()

+{

+  if (*)

+  {

+    assert true;

+  }

+  else

+  {

+    assert 0 != 0;  // error

+  }

+}

diff --git a/Test/dafny0/snapshots/runtest.snapshot b/Test/dafny0/snapshots/runtest.snapshot
index c3cf6b00..2d1cbe02 100644
--- a/Test/dafny0/snapshots/runtest.snapshot
+++ b/Test/dafny0/snapshots/runtest.snapshot
@@ -1,2 +1,2 @@
-// RUN: %dafny /compile:0 /verifySnapshots:2 /verifySeparately Snapshots0.dfy Snapshots1.dfy Snapshots2.dfy > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /verifySeparately Snapshots0.dfy Snapshots1.dfy Snapshots2.dfy Snapshots3.dfy > "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect
index 87827811..963ba754 100644
--- a/Test/dafny0/snapshots/runtest.snapshot.expect
+++ b/Test/dafny0/snapshots/runtest.snapshot.expect
@@ -25,3 +25,17 @@ Execution trace:
     (0,0): anon0

 

 Dafny program verifier finished with 5 verified, 1 error

+

+-------------------- Snapshots3.dfy --------------------

+Snapshots3.v0.dfy(9,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+

+Dafny program verifier finished with 1 verified, 1 error

+Snapshots3.v1.dfy(9,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+

+Dafny program verifier finished with 1 verified, 1 error