summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-03-13 10:29:03 -0700
committerGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-03-13 10:29:03 -0700
commitabf766e4b1b81e7327f7a23d16ddf35e39ecb1b4 (patch)
treedce69b75759f9b81cb5b760090ca2d167c4dfd12 /Source
parentdf2694faaf9b53d4b609270c431c76ec5b2068ff (diff)
Added explicit mod set analysis calls to OG transform and linear transform
Diffstat (limited to 'Source')
-rw-r--r--Source/Core/LinearSets.cs2
-rw-r--r--Source/Core/OwickiGries.cs2
2 files changed, 4 insertions, 0 deletions
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index f30336e5..d4c12ee0 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -453,6 +453,8 @@ namespace Microsoft.Boogie
var eraser = new LinearEraser();
eraser.VisitProgram(program);
+
+ Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);
}
private Expr Singleton(Expr e, string domainName)
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index 7182df3c..c0dd1164 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -556,6 +556,8 @@ namespace Microsoft.Boogie
{
program.TopLevelDeclarations.Add(proc);
}
+
+ Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);
}
}
}