Pyright static analysis reports a "possibly unbound variable" warning for the loop variable `i` in the `abbreviate_atoms` function. The variable is accessed after the inner loop terminates to slice the atom string. While the loop logic currently ensures execution, the analyzer flags the reliance on the loop variable persisting outside its scope.
Refactor the prefix length calculation into a nested `find_share_length` helper function. This encapsulates the search logic and uses explicit return statements, ensuring the length value is strictly defined. This satisfies the type checker and improves code readability without altering the runtime behavior. Signed-off-by: Wander Lairson Costa <[email protected]> --- tools/verification/rvgen/rvgen/ltl2k.py | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py index fa9ea6d597095..2c564cc937235 100644 --- a/tools/verification/rvgen/rvgen/ltl2k.py +++ b/tools/verification/rvgen/rvgen/ltl2k.py @@ -43,13 +43,17 @@ def abbreviate_atoms(atoms: list[str]) -> list[str]: skip = ["is", "by", "or", "and"] return '_'.join([x[:2] for x in s.lower().split('_') if x not in skip]) - abbrs = [] - for atom in atoms: + def find_share_length(atom: str) -> int: for i in range(len(atom), -1, -1): if sum(a.startswith(atom[:i]) for a in atoms) > 1: - break - share = atom[:i] - unique = atom[i:] + return i + return 0 + + abbrs = [] + for atom in atoms: + share_len = find_share_length(atom) + share = atom[:share_len] + unique = atom[share_len:] abbrs.append((shorten(share) + shorten(unique))) return abbrs -- 2.52.0
