Re: [PATCH v2 18/20] rv/rvgen: fix unbound loop variable warning

[Gabriele Monaco <gmonaco@redhat.com>]

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
>