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 <wander@redhat.com>
Looks good, that's probably the pythonic way then!
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
> ---
> 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
>