From b31dfdd5f4d30bd0c163c7955a6b7a9d9d024aaf Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 13 Nov 2025 13:09:44 +0100 Subject: [PATCH] Guards: Add elaborating comment. --- shared/controlflow/codeql/controlflow/Guards.qll | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index db81aa8443a..8fd39279ff6 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -1114,6 +1114,11 @@ module Make< private predicate validReturnInCustomGuardToRank( int rnk, NonOverridableMethod m, ParameterPosition ppos, GuardValue retval, GuardValue val ) { + // The forall-range has been pushed all the way into + // `relevantReturnExprValue` and `validReturnInCustomGuard`. This means + // that this base case ensures that at least one return expression + // non-vacuously satisfies that it's a valid implication from return + // value to parameter value. validReturnInCustomGuard(_, _, m, ppos, retval, val) and rnk = 0 or validReturnInCustomGuardToRank(rnk - 1, m, ppos, retval, val) and