On Wed, 2026-02-04 at 11:42 -0300, Wander Lairson Costa wrote: > 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]>
Looks good, that's probably the pythonic way then! Reviewed-by: Gabriele Monaco <[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 >
