diff options
author | Ally Donaldson <unknown> | 2014-03-05 16:57:11 +0000 |
---|---|---|
committer | Ally Donaldson <unknown> | 2014-03-05 16:57:11 +0000 |
commit | 84062edef96de98481916fc31080efe516a28948 (patch) | |
tree | 1305d460e5da4693c83ca99e1788afff5fc400b7 /Source | |
parent | b30f6fdc354d3abd09204f8a9b80c05913da26a4 (diff) |
Fix to predication
Diffstat (limited to 'Source')
-rw-r--r-- | Source/Predication/SmartBlockPredicator.cs | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs index ea526591..37161f05 100644 --- a/Source/Predication/SmartBlockPredicator.cs +++ b/Source/Predication/SmartBlockPredicator.cs @@ -79,6 +79,7 @@ public class SmartBlockPredicator { cCmd.Ins.Insert(0, p != null ? p : Expr.True);
cmdSeq.Add(cCmd);
} else if (p == null) {
+ new EnabledReplacementVisitor(Expr.True).Visit(cmd);
cmdSeq.Add(cmd);
} else if (cmd is AssignCmd) {
var aCmd = (AssignCmd)cmd;
@@ -224,7 +225,7 @@ public class SmartBlockPredicator { return;
}
}
-
+
if (uni != null && uni.IsUniform(impl.Name, block.Item1)) {
if (blockGraph.Headers.Contains(block.Item1)) {
parentMap[block.Item1] = header;
@@ -520,6 +521,15 @@ public class SmartBlockPredicator { }
}
}
+ } else {
+ if (impl == null) {
+ foreach (Requires r in proc.Requires) {
+ new EnabledReplacementVisitor(Expr.True).VisitExpr(r.Condition);
+ }
+ foreach (Ensures e in proc.Ensures) {
+ new EnabledReplacementVisitor(Expr.True).VisitExpr(e.Condition);
+ }
+ }
}
if (impl != null) {
|