Patch by Jeroen Ketema.

Drop the “basic” block predication algorithm. Block predication is only used
by GPUVerify, and then only in the “smart” version as the basic algorithm does
not perform very well. As a consequence this code is essentially dead.

1 files changed, 28 insertions, 0 deletions

diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs
index 7579158d..739f0e2b 100644
--- a/Source/Predication/SmartBlockPredicator.cs
+++ b/Source/Predication/SmartBlockPredicator.cs
@@ -606,4 +606,32 @@ public class SmartBlockPredicator {
 

 }

 

+class EnabledReplacementVisitor : StandardVisitor

+{

+    private Expr pExpr;

+    private Expr pDomExpr;

+

+    internal EnabledReplacementVisitor(Expr pExpr, Expr pDomExpr)

+    {

+        this.pExpr = pExpr;

+        this.pDomExpr = pDomExpr;

+    }

+

+    public override Expr VisitExpr(Expr node)

+    {

+        if (node is IdentifierExpr)

+        {

+            IdentifierExpr iExpr = node as IdentifierExpr;

+            if (iExpr.Decl is Constant && QKeyValue.FindBoolAttribute(iExpr.Decl.Attributes, "__enabled"))

+            {

+                return pExpr;

+            } else if (iExpr.Decl is Constant && QKeyValue.FindBoolAttribute(iExpr.Decl.Attributes, "__dominator_enabled"))

+            {

+                return pDomExpr;

+            }

+        }

+        return base.VisitExpr(node);

+    }

+}

+

 }