From 9dd6232267e919a14321b07950ad7860bc29b082 Mon Sep 17 00:00:00 2001
From: allydonaldson <unknown>
Date: Fri, 1 Mar 2013 09:57:46 +0000
Subject: Fixed bug with predication, and fixed small problem with model
 generation related to casting

---
 Source/Predication/SmartBlockPredicator.cs | 22 +++++++++++++++++-----
 1 file changed, 17 insertions(+), 5 deletions(-)

(limited to 'Source/Predication')

diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs
index 834099ff..55e73161 100644
--- a/Source/Predication/SmartBlockPredicator.cs
+++ b/Source/Predication/SmartBlockPredicator.cs
@@ -94,7 +94,9 @@ public class SmartBlockPredicator {
       cmdSeq.Add(aCmd);
     } else if (cmd is AssumeCmd) {
       var aCmd = (AssumeCmd)cmd;
-      cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));
+      Expr newExpr = new EnabledReplacementVisitor(p).VisitExpr(aCmd.Expr);
+      aCmd.Expr = QKeyValue.FindBoolAttribute(aCmd.Attributes, "do_not_predicate") ? newExpr : Expr.Imp(p, newExpr);
+      cmdSeq.Add(aCmd);
     } else if (cmd is HavocCmd) {
       var hCmd = (HavocCmd)cmd;
       foreach (IdentifierExpr v in hCmd.Vars) {
@@ -216,12 +218,22 @@ public class SmartBlockPredicator {
 
     while (i.MoveNext()) {
       var block = i.Current;
-      if (uni != null && uni.IsUniform(impl.Name, block.Item1))
-        continue;
+
       if (block.Item2) {
-        if (block.Item1 == header)
+        if (block.Item1 == header) {
           return;
-      } else {
+        }
+      }
+     
+      if (uni != null && uni.IsUniform(impl.Name, block.Item1)) {
+        if (blockGraph.Headers.Contains(block.Item1)) {
+          parentMap[block.Item1] = header;
+          AssignPredicates(blockGraph, dom, pdom, i, headPredicate, ref predCount);
+        }
+        continue;
+      }
+
+      if (!block.Item2) {
         if (blockGraph.Headers.Contains(block.Item1)) {
           parentMap[block.Item1] = header;
           var loopPred = FreshPredicate(ref predCount);
-- 
cgit v1.2.3