fix some QL-for-QL warnings

This commit is contained in:
erik-krogh
2022-08-12 20:38:50 +02:00
parent b54f037424
commit 3a4a3437b5
7 changed files with 26 additions and 12 deletions

View File

@@ -7,6 +7,8 @@ import regexp.RegexpMatching
/**
* Holds if the regexp `root` should be tested against `str`.
* Implements the `isRegexpMatchingCandidateSig` signature from `RegexpMatching`.
* `ignorePrefix` toggles whether the regular expression should be treated as accepting any prefix if it's unanchored.
* `testWithGroups` toggles whether it's tested which groups are filled by a given input string.
*/
private predicate isBadTagFilterCandidate(
RootTerm root, string str, boolean ignorePrefix, boolean testWithGroups

View File

@@ -267,10 +267,12 @@ int distBackFromEnd(StateTuple r, StateTuple end) =
* and there is a distance of `dist` from `tuple` to the nearest end-tuple `(pivot, succ, succ)`,
* and a path from a start-state to `tuple` follows the transitions in `trace`.
*/
private predicate isReachableFromStartTuple(State pivot, State succ, StateTuple r, Trace w, int rem) {
private predicate isReachableFromStartTuple(
State pivot, State succ, StateTuple tuple, Trace trace, int dist
) {
exists(InputSymbol s1, InputSymbol s2, InputSymbol s3, Trace v |
isReachableFromStartTuple(pivot, succ, v, s1, s2, s3, r, rem) and
w = Step(s1, s2, s3, v)
isReachableFromStartTuple(pivot, succ, v, s1, s2, s3, tuple, dist) and
trace = Step(s1, s2, s3, v)
)
}