From 23471ff664051f15faee787eb25ca72b74acfab5 Mon Sep 17 00:00:00 2001
From: Unknown <afd@afd-THINK.home>
Date: Thu, 20 Dec 2012 09:24:02 +0000
Subject: Support for "do_not_predicate" in predication of requires and ensures

---
 Source/Predication/SmartBlockPredicator.cs | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'Source/Predication')

diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs
index 2150f72d..834099ff 100644
--- a/Source/Predication/SmartBlockPredicator.cs
+++ b/Source/Predication/SmartBlockPredicator.cs
@@ -494,11 +494,18 @@ public class SmartBlockPredicator {
               .ToArray());
 
           if (impl == null) {
+            var fpIdentifierExpr = new IdentifierExpr(Token.NoToken, fpVar);
             foreach (Requires r in proc.Requires) {
-              new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(r.Condition);
+              new EnabledReplacementVisitor(fpIdentifierExpr).VisitExpr(r.Condition);
+              if (!QKeyValue.FindBoolAttribute(r.Attributes, "do_not_predicate")) {
+                r.Condition = Expr.Imp(fpIdentifierExpr, r.Condition);
+              }
             }
             foreach (Ensures e in proc.Ensures) {
               new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(e.Condition);
+              if (!QKeyValue.FindBoolAttribute(e.Attributes, "do_not_predicate")) {
+                e.Condition = Expr.Imp(fpIdentifierExpr, e.Condition);
+              }
             }
           }
         }
-- 
cgit v1.2.3