diff options
| author |  Akash Lal <akashl@microsoft.com> | 2015-06-05 10:09:41 +0530 |
|---|---|---|
| committer | Akash Lal <akashl@microsoft.com> | 2015-06-05 10:09:41 +0530 |
| commit | b42d69a32e0e3a8132fd4b1288618fe4a7392eb6 (patch) | |
| tree | 5b0118e1b191920f1c1c54288046846e03099ea5 /Source | |
| parent | c8eb509045eccd1b44fd335f9e1ef5cf80d7cd89 (diff) | |
Fix for SI: initialize extraRecBound
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 18 |
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
|