From 1ef98ea7e0c89a39a90a9d0501bb1a806e156e8a Mon Sep 17 00:00:00 2001
From: Mathias Vorreiter Pedersen <mathiasvp@github.com>
Date: Tue, 26 Apr 2022 13:59:17 +0100
Subject: [PATCH] C++: Fix join order in 'bbSuccessorEntryReaches'.

---
 .../code/cpp/controlflow/StackVariableReachability.qll      | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/controlflow/StackVariableReachability.qll b/cpp/ql/lib/semmle/code/cpp/controlflow/StackVariableReachability.qll
index 373ab8b79e2e..c88be4c7d6eb 100644
--- a/cpp/ql/lib/semmle/code/cpp/controlflow/StackVariableReachability.qll
+++ b/cpp/ql/lib/semmle/code/cpp/controlflow/StackVariableReachability.qll
@@ -92,6 +92,7 @@ abstract class StackVariableReachability extends string {
     )
   }
 
+  pragma[nomagic]
   private predicate bbSuccessorEntryReaches(
     BasicBlock bb, SemanticStackVariable v, ControlFlowNode node,
     boolean skipsFirstLoopAlwaysTrueUponEntry
@@ -103,8 +104,9 @@ abstract class StackVariableReachability extends string {
       this.bbEntryReachesLocally(succ, v, node) and
       succSkipsFirstLoopAlwaysTrueUponEntry = false
       or
-      not this.isBarrier(succ.getNode(_), v) and
-      this.bbSuccessorEntryReaches(succ, v, node, succSkipsFirstLoopAlwaysTrueUponEntry)
+      not this.isBarrier(succ.getNode(_), pragma[only_bind_into](v)) and
+      this.bbSuccessorEntryReaches(succ, pragma[only_bind_into](v), node,
+        succSkipsFirstLoopAlwaysTrueUponEntry)
     )
   }