Allow the provider to skip some states when generating SourceLocations

3 files changed, 10 insertions, 6 deletions

diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs
index 50783c44..721ee182 100644
--- a/Source/ModelViewer/DafnyProvider.cs
+++ b/Source/ModelViewer/DafnyProvider.cs
@@ -24,6 +24,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
         var sn = new StateNode(dm.states.Count, dm, s);

         dm.states.Add(sn);

       }

+      dm.FinishStates();

       return dm;

     }

   }

@@ -77,6 +78,11 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
       }

     }

 

+    internal void FinishStates()

+    {

+      GenerateSourceLocations(states);

+    }

+

     public override IEnumerable<IState> States

     {

       get { return states; }

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index 621f3837..f6858003 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -18,7 +18,7 @@ namespace Microsoft.Boogie.ModelViewer
     protected Dictionary<Model.Element, string> canonicalName = new Dictionary<Model.Element, string>();

     protected Dictionary<string, Model.Element> invCanonicalName = new Dictionary<string, Model.Element>();

     protected Dictionary<Model.Element, string> localValue = new Dictionary<Model.Element, string>();

-    protected Dictionary<string, SourceLocation> sourceLocations; // initialized lazily by GetSourceLocation()

+    protected Dictionary<string, SourceLocation> sourceLocations = new Dictionary<string, SourceLocation>();

     public readonly Model model;

 

     protected virtual bool UseLocalsForCanonicalNames

@@ -248,10 +248,6 @@ namespace Microsoft.Boogie.ModelViewer
 

     public SourceLocation GetSourceLocation(Model.CapturedState s)

     {

-      if (sourceLocations == null) {

-        GenerateSourceLocations();

-      }

-

       SourceLocation res;

       sourceLocations.TryGetValue(s.Name, out res);

       return res;

@@ -329,7 +325,7 @@ namespace Microsoft.Boogie.ModelViewer
       sb.Append(@"{\cf6 ").Append(n).Append("}");

     }

 

-    protected virtual void GenerateSourceLocations()

+    protected virtual void GenerateSourceLocations(IEnumerable<NamedState> states)

     {

       sourceLocations = new Dictionary<string, SourceLocation>();

 

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index ff7c6626..4395041f 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -125,6 +125,8 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         var sn = new StateNode(states.Count, this, s);

         states.Add(sn);

       }

+

+      GenerateSourceLocations(states);

     }

 

     #region Function name scoring