summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar Akash Lal <akashl@microsoft.com>2015-06-05 10:09:41 +0530
committerGravatar Akash Lal <akashl@microsoft.com>2015-06-05 10:09:41 +0530
commitb42d69a32e0e3a8132fd4b1288618fe4a7392eb6 (patch)
tree5b0118e1b191920f1c1c54288046846e03099ea5 /Source
parentc8eb509045eccd1b44fd335f9e1ef5cf80d7cd89 (diff)
Fix for SI: initialize extraRecBound
Diffstat (limited to 'Source')
-rw-r--r--Source/VCGeneration/StratifiedVC.cs18
1 files changed, 9 insertions, 9 deletions
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index da2c37c6..037fa2be 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -837,15 +837,7 @@ namespace VC {
public StratifiedVCGen(bool usePrevCallTree, HashSet<string> prevCallTree,
Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
: this(program, logFilePath, appendLogFile, checkers)
- {
- this.extraRecBound = new Dictionary<string, int>();
- program.TopLevelDeclarations.OfType<Implementation>()
- .Iter(impl =>
- {
- var b = QKeyValue.FindIntAttribute(impl.Attributes, "SIextraRecBound", -1);
- if(b != -1) extraRecBound.Add(impl.Name, b);
- });
-
+ {
if (usePrevCallTree) {
callTree = prevCallTree;
PersistCallTree = true;
@@ -859,6 +851,14 @@ namespace VC {
: base(program, logFilePath, appendLogFile, checkers, null) {
PersistCallTree = false;
procsThatReachedRecBound = new HashSet<string>();
+
+ extraRecBound = new Dictionary<string, int>();
+ program.TopLevelDeclarations.OfType<Implementation>()
+ .Iter(impl =>
+ {
+ var b = QKeyValue.FindIntAttribute(impl.Attributes, "SIextraRecBound", -1);
+ if (b != -1) extraRecBound.Add(impl.Name, b);
+ });
}
// Extra rec bound for procedures