DafnyExtension: Worked on integrating the verification result caching.

2 files changed, 18 insertions, 2 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 688b599c..5833b41e 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2167,6 +2167,8 @@ namespace Microsoft.Dafny {
       }

       var checksum = string.Join("", md5.Hash);

       decl.AddAttribute("checksum", checksum);

+

+      InsertUniqueIdForImplementation(decl);

     }

 

     private static void InsertChecksum(Function f, Bpl.Declaration decl, bool specificationOnly = false)

@@ -2188,6 +2190,17 @@ namespace Microsoft.Dafny {
       }

       var checksum = string.Join("", md5.Hash);

       decl.AddAttribute("checksum", checksum);

+

+      InsertUniqueIdForImplementation(decl);

+    }

+

+    public static void InsertUniqueIdForImplementation(Bpl.Declaration decl)

+    {

+      var impl = decl as Bpl.Implementation;

+      if (impl != null && !string.IsNullOrEmpty(impl.tok.filename))

+      {

+        decl.AddAttribute("id", impl.tok.filename + ":" + impl.Id);

+      }

     }

 

     void CheckFrameWellFormed(List<FrameExpression> fes, VariableSeq locals, StmtListBuilder builder, ExpressionTranslator etran) {

diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index e38d9eea..8a8c753b 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -4,6 +4,7 @@ using System.Collections.Generic;
 using System.ComponentModel.Composition;

 using System.Diagnostics.Contracts;

 using System.Linq;

+using System.Text.RegularExpressions;

 using System.Threading;

 using System.Windows;

 using System.Windows.Media;

@@ -255,8 +256,10 @@ namespace DafnyLanguage
         bufferChangesPostVerificationStart.Clear();

         bufferChangesPostVerificationStart.Add(new SnapshotSpan(_buffer.CurrentSnapshot, 0, _buffer.CurrentSnapshot.Length));

         verificationDisabled = false;

-        // TODO(wuestholz): Only drop verification results from this buffer.

-        Microsoft.Boogie.ExecutionEngine.EmptyCache();

+        if (_document != null)

+        {

+          Microsoft.Boogie.ExecutionEngine.RemoveMatchingKeysFromCache(new Regex(string.Format(@"^{0}", Regex.Escape(_document.FilePath))));

+        }

         NotifyAboutChangedTags(_buffer.CurrentSnapshot);

       }

     }