diff options
author | MichalMoskal <unknown> | 2011-01-26 23:30:07 +0000 |
---|---|---|
committer | MichalMoskal <unknown> | 2011-01-26 23:30:07 +0000 |
commit | 34e214d35927c2cf49efdab79d111c67ae283ce7 (patch) | |
tree | b9e86c3996c13b9cfb192dfa22d434a59d781283 /Source/ModelViewer | |
parent | 950c133dba480d0ff4e99fe56096feeee95172ae (diff) |
Allow the provider to skip some states when generating SourceLocations
Diffstat (limited to 'Source/ModelViewer')
-rw-r--r-- | Source/ModelViewer/DafnyProvider.cs | 6 | ||||
-rw-r--r-- | Source/ModelViewer/Namer.cs | 8 | ||||
-rw-r--r-- | Source/ModelViewer/VccProvider.cs | 2 |
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
|