Java: Adjust Paths.qll

This commit is contained in:
Anders Schack-Mulligen
2025-07-16 14:49:20 +02:00
parent e7a6259bd7
commit 54775e0958

View File

@@ -66,6 +66,10 @@ private class JoinBlock extends BasicBlock {
JoinBlock() { 2 <= strictcount(this.getAPredecessor()) }
}
private class ReachableBlock extends BasicBlock {
ReachableBlock() { hasDominanceInformation(this) }
}
/**
* Holds if `bb` is a block that is collectively dominated by a set of one or
* more actions that individually does not dominate the exit.
@@ -74,7 +78,7 @@ private predicate postActionBlock(BasicBlock bb, ActionConfiguration conf) {
bb = nonDominatingActionBlock(conf)
or
if bb instanceof JoinBlock
then forall(BasicBlock pred | pred = bb.getAPredecessor() | postActionBlock(pred, conf))
then forall(ReachableBlock pred | pred = bb.getAPredecessor() | postActionBlock(pred, conf))
else postActionBlock(bb.getAPredecessor(), conf)
}