@@ -214,6 +214,7 @@ abstract class Configuration extends string {
214214 * Holds if `guard` is a barrier guard for this configuration, added through
215215 * `isBarrierGuard` or `AdditionalBarrierGuardNode`.
216216 */
217+ pragma [ nomagic]
217218 private predicate isBarrierGuardInternal ( BarrierGuardNode guard ) {
218219 isBarrierGuard ( guard )
219220 or
@@ -368,6 +369,7 @@ abstract class BarrierGuardNode extends DataFlow::Node {
368369 *
369370 * `label` is bound to the blocked label, or the empty string if all labels should be blocked.
370371 */
372+ pragma [ nomagic]
371373private predicate barrierGuardBlocksExpr (
372374 BarrierGuardNode guard , boolean outcome , Expr test , string label
373375) {
@@ -383,7 +385,7 @@ private predicate barrierGuardBlocksExpr(
383385/**
384386 * Holds if `guard` may block the flow of a value reachable through exploratory flow.
385387 */
386- pragma [ noinline ]
388+ pragma [ nomagic ]
387389private predicate barrierGuardIsRelevant ( BarrierGuardNode guard ) {
388390 exists ( Expr e |
389391 barrierGuardBlocksExpr ( guard , _, e , _) and
@@ -397,7 +399,7 @@ private predicate barrierGuardIsRelevant(BarrierGuardNode guard) {
397399 *
398400 * `label` is bound to the blocked label, or the empty string if all labels should be blocked.
399401 */
400- pragma [ noinline ]
402+ pragma [ nomagic ]
401403private predicate barrierGuardBlocksAccessPath (
402404 BarrierGuardNode guard , boolean outcome , AccessPath ap , string label
403405) {
@@ -410,6 +412,7 @@ private predicate barrierGuardBlocksAccessPath(
410412 *
411413 * This predicate is outlined to give the optimizer a hint about the join ordering.
412414 */
415+ pragma [ nomagic]
413416private predicate barrierGuardBlocksSsaRefinement (
414417 BarrierGuardNode guard , boolean outcome , SsaRefinementNode ref , string label
415418) {
@@ -425,7 +428,7 @@ private predicate barrierGuardBlocksSsaRefinement(
425428 *
426429 * `outcome` is bound to the outcome of `cond` for join-ordering purposes.
427430 */
428- pragma [ noinline ]
431+ pragma [ nomagic ]
429432private predicate barrierGuardUsedInCondition (
430433 BarrierGuardNode guard , ConditionGuardNode cond , boolean outcome
431434) {
@@ -444,6 +447,7 @@ private predicate barrierGuardUsedInCondition(
444447 *
445448 * `label` is bound to the blocked label, or the empty string if all labels should be blocked.
446449 */
450+ pragma [ nomagic]
447451private predicate barrierGuardBlocksNode ( BarrierGuardNode guard , DataFlow:: Node nd , string label ) {
448452 // 1) `nd` is a use of a refinement node that blocks its input variable
449453 exists ( SsaRefinementNode ref , boolean outcome |
@@ -466,6 +470,7 @@ private predicate barrierGuardBlocksNode(BarrierGuardNode guard, DataFlow::Node
466470 *
467471 * `label` is bound to the blocked label, or the empty string if all labels should be blocked.
468472 */
473+ pragma [ nomagic]
469474private predicate barrierGuardBlocksEdge (
470475 BarrierGuardNode guard , DataFlow:: Node pred , DataFlow:: Node succ , string label
471476) {
0 commit comments