Avoid computing join points when it's not needed

viperproject · Jun 17, 2024 · 422c431 · 422c431
1 parent c4350bd
commit 422c431
Showing 1 changed file with 6 additions and 2 deletions.
diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
@@ -106,8 +106,12 @@ object executor extends ExecutionRules {
                      (Q: (State, Verifier) => VerificationResult)
                      : VerificationResult = {
 
-    // Find join point if it exists.
-    val jp: Option[SilverBlock] = edges.headOption.flatMap(edge => s.methodCfg.joinPoints.get(edge.source))
+    // If joining branches is enabled, find join point if it exists.
+    val jp: Option[SilverBlock] = if (s.moreJoins.id >= JoinMode.All.id) {
+      edges.headOption.flatMap(edge => s.methodCfg.joinPoints.get(edge.source))
+    } else {
+      None
+    }
 
     (edges, jp) match {
       case (Seq(), _) => Q(s, v)