Skip to content

Commit b31dfdd

Browse files
committed
Guards: Add elaborating comment.
1 parent 62e28d2 commit b31dfdd

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

shared/controlflow/codeql/controlflow/Guards.qll

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1114,6 +1114,11 @@ module Make<
11141114
private predicate validReturnInCustomGuardToRank(
11151115
int rnk, NonOverridableMethod m, ParameterPosition ppos, GuardValue retval, GuardValue val
11161116
) {
1117+
// The forall-range has been pushed all the way into
1118+
// `relevantReturnExprValue` and `validReturnInCustomGuard`. This means
1119+
// that this base case ensures that at least one return expression
1120+
// non-vacuously satisfies that it's a valid implication from return
1121+
// value to parameter value.
11171122
validReturnInCustomGuard(_, _, m, ppos, retval, val) and rnk = 0
11181123
or
11191124
validReturnInCustomGuardToRank(rnk - 1, m, ppos, retval, val) and

0 commit comments

Comments
 (0)