Initialize loop variable `i` before the for loop in abbreviate_atoms
function to fix pyright static type checker error. The previous code
left `i` potentially unbound in edge cases where the range could be
empty, though this would not occur in practice since the loop always
executes at least once with the given range parameters.

The initialization to zero ensures that `i` has a defined value before
entering the loop scope, satisfying static analysis requirements
while preserving the existing logic. The for loop immediately assigns
i to the first value from the range, so the initialization value is
never actually used in normal execution paths.

This change resolves the pyright reportPossiblyUnbound error without
altering the function's behavior or performance characteristics.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
---
 tools/verification/rvgen/rvgen/ltl2k.py | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py
index fa9ea6d597095..94dc64af1716d 100644
--- a/tools/verification/rvgen/rvgen/ltl2k.py
+++ b/tools/verification/rvgen/rvgen/ltl2k.py
@@ -45,6 +45,7 @@ def abbreviate_atoms(atoms: list[str]) -> list[str]:
 
     abbrs = []
     for atom in atoms:
+        i = 0
         for i in range(len(atom), -1, -1):
             if sum(a.startswith(atom[:i]) for a in atoms) > 1:
                 break
-- 
2.52.0

Wander Lairson Costa <wander@redhat.com> writes:

> Initialize loop variable `i` before the for loop in abbreviate_atoms
> function to fix pyright static type checker error. The previous code
> left `i` potentially unbound in edge cases where the range could be
> empty, though this would not occur in practice since the loop always
> executes at least once with the given range parameters.
>
> The initialization to zero ensures that `i` has a defined value before
> entering the loop scope, satisfying static analysis requirements
> while preserving the existing logic. The for loop immediately assigns
> i to the first value from the range, so the initialization value is
> never actually used in normal execution paths.
>
> This change resolves the pyright reportPossiblyUnbound error without
> altering the function's behavior or performance characteristics.
>
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>

I understand this is just to suppress a false warning, not fixing real
problem.

Reviewed-by: Nam Cao <namcao@linutronix.de>

On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:
> Initialize loop variable `i` before the for loop in abbreviate_atoms
> function to fix pyright static type checker error. The previous code
> left `i` potentially unbound in edge cases where the range could be
> empty, though this would not occur in practice since the loop always
> executes at least once with the given range parameters.
> 
> The initialization to zero ensures that `i` has a defined value before
> entering the loop scope, satisfying static analysis requirements
> while preserving the existing logic. The for loop immediately assigns
> i to the first value from the range, so the initialization value is
> never actually used in normal execution paths.
> 
> This change resolves the pyright reportPossiblyUnbound error without
> altering the function's behavior or performance characteristics.

So are we just pleasing the tool or is there a real implication of this?

Apparently code like

for i in range(len([]), -1, -1):
    pass
print(i)

works just fine since range() returns at least 0 (as you mentioned in the commit
message) and i is not used before assignation in the loop, so I don't really see
a problem.

Apparently pyright devs don't want ([1]) to implement a logic to sort out the
/possibly/ unbound error here.

From what I understand, this code is already not pythonic, so rather than
silence the warning to please this tool I'd just refactor the code not to use i
after the loop (or leave it as it is, since it works fine).

What do you think?

Thanks,
Gabriele

[1] - https://github.com/microsoft/pyright/issues/844

> 
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>
> ---
>  tools/verification/rvgen/rvgen/ltl2k.py | 1 +
>  1 file changed, 1 insertion(+)
> 
> diff --git a/tools/verification/rvgen/rvgen/ltl2k.py
> b/tools/verification/rvgen/rvgen/ltl2k.py
> index fa9ea6d597095..94dc64af1716d 100644
> --- a/tools/verification/rvgen/rvgen/ltl2k.py
> +++ b/tools/verification/rvgen/rvgen/ltl2k.py
> @@ -45,6 +45,7 @@ def abbreviate_atoms(atoms: list[str]) -> list[str]:
>  
>      abbrs = []
>      for atom in atoms:
> +        i = 0
>          for i in range(len(atom), -1, -1):
>              if sum(a.startswith(atom[:i]) for a in atoms) > 1:
>                  break

On Tue, Jan 20, 2026 at 09:59:11AM +0100, Gabriele Monaco wrote:
> On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:
> > Initialize loop variable `i` before the for loop in abbreviate_atoms
> > function to fix pyright static type checker error. The previous code
> > left `i` potentially unbound in edge cases where the range could be
> > empty, though this would not occur in practice since the loop always
> > executes at least once with the given range parameters.
> > 
> > The initialization to zero ensures that `i` has a defined value before
> > entering the loop scope, satisfying static analysis requirements
> > while preserving the existing logic. The for loop immediately assigns
> > i to the first value from the range, so the initialization value is
> > never actually used in normal execution paths.
> > 
> > This change resolves the pyright reportPossiblyUnbound error without
> > altering the function's behavior or performance characteristics.
> 
> So are we just pleasing the tool or is there a real implication of this?
> 
> Apparently code like
> 
> for i in range(len([]), -1, -1):
>     pass
> print(i)
> 
> works just fine since range() returns at least 0 (as you mentioned in the commit
> message) and i is not used before assignation in the loop, so I don't really see
> a problem.
> 
> Apparently pyright devs don't want ([1]) to implement a logic to sort out the
> /possibly/ unbound error here.
> 
> From what I understand, this code is already not pythonic, so rather than
> silence the warning to please this tool I'd just refactor the code not to use i
> after the loop (or leave it as it is, since it works fine).
> 
> What do you think?

You're right, I could have done:

for atom in reversed(atoms): ...

I will modify it in v2.

> 
> Thanks,
> Gabriele
> 
> [1] - https://github.com/microsoft/pyright/issues/844
> 
> > 
> > Signed-off-by: Wander Lairson Costa <wander@redhat.com>
> > ---
> >  tools/verification/rvgen/rvgen/ltl2k.py | 1 +
> >  1 file changed, 1 insertion(+)
> > 
> > diff --git a/tools/verification/rvgen/rvgen/ltl2k.py
> > b/tools/verification/rvgen/rvgen/ltl2k.py
> > index fa9ea6d597095..94dc64af1716d 100644
> > --- a/tools/verification/rvgen/rvgen/ltl2k.py
> > +++ b/tools/verification/rvgen/rvgen/ltl2k.py
> > @@ -45,6 +45,7 @@ def abbreviate_atoms(atoms: list[str]) -> list[str]:
> >  
> >      abbrs = []
> >      for atom in atoms:
> > +        i = 0
> >          for i in range(len(atom), -1, -1):
> >              if sum(a.startswith(atom[:i]) for a in atoms) > 1:
> >                  break
> 

On Tue, 2026-01-20 at 08:37 -0300, Wander Lairson Costa wrote:
> On Tue, Jan 20, 2026 at 09:59:11AM +0100, Gabriele Monaco wrote:
> > On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:
> > > Initialize loop variable `i` before the for loop in abbreviate_atoms
> > > function to fix pyright static type checker error. The previous code
> > > left `i` potentially unbound in edge cases where the range could be
> > > empty, though this would not occur in practice since the loop always
> > > executes at least once with the given range parameters.
> > > 
> > > The initialization to zero ensures that `i` has a defined value before
> > > entering the loop scope, satisfying static analysis requirements
> > > while preserving the existing logic. The for loop immediately assigns
> > > i to the first value from the range, so the initialization value is
> > > never actually used in normal execution paths.
> > > 
> > > This change resolves the pyright reportPossiblyUnbound error without
> > > altering the function's behavior or performance characteristics.
> > 
> > So are we just pleasing the tool or is there a real implication of this?
> > 
> > Apparently code like
> > 
> > for i in range(len([]), -1, -1):
> >     pass
> > print(i)
> > 
> > works just fine since range() returns at least 0 (as you mentioned in the
> > commit
> > message) and i is not used before assignation in the loop, so I don't really
> > see
> > a problem.
> > 
> > Apparently pyright devs don't want ([1]) to implement a logic to sort out
> > the
> > /possibly/ unbound error here.
> > 
> > From what I understand, this code is already not pythonic, so rather than
> > silence the warning to please this tool I'd just refactor the code not to
> > use i
> > after the loop (or leave it as it is, since it works fine).
> > 
> > What do you think?
> 
> You're right, I could have done:
> 
> for atom in reversed(atoms): ...
> 

I'm missing what you mean with this, the range is iterating over the string
representation of atom (in reverse) not the array of atoms.

You basically want i to be the length of the longest prefix common to at least
another atom.

You could assign i to some python trick doing the exact same thing the loop
does, like:

    i = next((i for i in range(len(atom), -1, -1)
        if sum(a.startswith(atom[:i]) for a in atoms) > 1))

next() is basically doing the break at the first occurrence from the generator,
just now your i doesn't live (only) inside the loop.

So now you save 2 lines and get any C developer scratch their head when they
look at the code, but hey, pyright is happy!

If you do find the trick with next() readable or have any better idea, feel free
to try though.

Thanks,
Gabriele

> I will modify it in v2.
> 
> > 
> > Thanks,
> > Gabriele
> > 
> > [1] - https://github.com/microsoft/pyright/issues/844
> > 
> > > 
> > > Signed-off-by: Wander Lairson Costa <wander@redhat.com>
> > > ---
> > >  tools/verification/rvgen/rvgen/ltl2k.py | 1 +
> > >  1 file changed, 1 insertion(+)
> > > 
> > > diff --git a/tools/verification/rvgen/rvgen/ltl2k.py
> > > b/tools/verification/rvgen/rvgen/ltl2k.py
> > > index fa9ea6d597095..94dc64af1716d 100644
> > > --- a/tools/verification/rvgen/rvgen/ltl2k.py
> > > +++ b/tools/verification/rvgen/rvgen/ltl2k.py
> > > @@ -45,6 +45,7 @@ def abbreviate_atoms(atoms: list[str]) -> list[str]:
> > >  
> > >      abbrs = []
> > >      for atom in atoms:
> > > +        i = 0
> > >          for i in range(len(atom), -1, -1):
> > >              if sum(a.startswith(atom[:i]) for a in atoms) > 1:
> > >                  break
> > 

On Tue, Jan 20, 2026 at 01:30:35PM +0100, Gabriele Monaco wrote:
> On Tue, 2026-01-20 at 08:37 -0300, Wander Lairson Costa wrote:
> > On Tue, Jan 20, 2026 at 09:59:11AM +0100, Gabriele Monaco wrote:
> > > On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:
> > > > Initialize loop variable `i` before the for loop in abbreviate_atoms
> > > > function to fix pyright static type checker error. The previous code
> > > > left `i` potentially unbound in edge cases where the range could be
> > > > empty, though this would not occur in practice since the loop always
> > > > executes at least once with the given range parameters.
> > > > 
> > > > The initialization to zero ensures that `i` has a defined value before
> > > > entering the loop scope, satisfying static analysis requirements
> > > > while preserving the existing logic. The for loop immediately assigns
> > > > i to the first value from the range, so the initialization value is
> > > > never actually used in normal execution paths.
> > > > 
> > > > This change resolves the pyright reportPossiblyUnbound error without
> > > > altering the function's behavior or performance characteristics.
> > > 
> > > So are we just pleasing the tool or is there a real implication of this?
> > > 
> > > Apparently code like
> > > 
> > > for i in range(len([]), -1, -1):
> > >     pass
> > > print(i)
> > > 
> > > works just fine since range() returns at least 0 (as you mentioned in the
> > > commit
> > > message) and i is not used before assignation in the loop, so I don't really
> > > see
> > > a problem.
> > > 
> > > Apparently pyright devs don't want ([1]) to implement a logic to sort out
> > > the
> > > /possibly/ unbound error here.
> > > 
> > > From what I understand, this code is already not pythonic, so rather than
> > > silence the warning to please this tool I'd just refactor the code not to
> > > use i
> > > after the loop (or leave it as it is, since it works fine).
> > > 
> > > What do you think?
> > 
> > You're right, I could have done:
> > 
> > for atom in reversed(atoms): ...
> > 
> 
> I'm missing what you mean with this, the range is iterating over the string
> representation of atom (in reverse) not the array of atoms.
> 

Sorry, I misinterpreted you previous comment and picked the wrong piece
of code.

Yes, the basic goal was to make pyright happy.

> You basically want i to be the length of the longest prefix common to at least
> another atom.
> 
> You could assign i to some python trick doing the exact same thing the loop
> does, like:
> 
>     i = next((i for i in range(len(atom), -1, -1)
>         if sum(a.startswith(atom[:i]) for a in atoms) > 1))
> 
> next() is basically doing the break at the first occurrence from the generator,
> just now your i doesn't live (only) inside the loop.
> 
> So now you save 2 lines and get any C developer scratch their head when they
> look at the code, but hey, pyright is happy!
> 

Or just leave the assignment.

> If you do find the trick with next() readable or have any better idea, feel free
> to try though.
> 

Definitely the next() trick is not worth to make pyright happy.

> Thanks,
> Gabriele
> 
> > I will modify it in v2.
> > 
> > > 
> > > Thanks,
> > > Gabriele
> > > 
> > > [1] - https://github.com/microsoft/pyright/issues/844
> > > 
> > > > 
> > > > Signed-off-by: Wander Lairson Costa <wander@redhat.com>
> > > > ---
> > > >  tools/verification/rvgen/rvgen/ltl2k.py | 1 +
> > > >  1 file changed, 1 insertion(+)
> > > > 
> > > > diff --git a/tools/verification/rvgen/rvgen/ltl2k.py
> > > > b/tools/verification/rvgen/rvgen/ltl2k.py
> > > > index fa9ea6d597095..94dc64af1716d 100644
> > > > --- a/tools/verification/rvgen/rvgen/ltl2k.py
> > > > +++ b/tools/verification/rvgen/rvgen/ltl2k.py
> > > > @@ -45,6 +45,7 @@ def abbreviate_atoms(atoms: list[str]) -> list[str]:
> > > >  
> > > >      abbrs = []
> > > >      for atom in atoms:
> > > > +        i = 0
> > > >          for i in range(len(atom), -1, -1):
> > > >              if sum(a.startswith(atom[:i]) for a in atoms) > 1:
> > > >                  break
> > > 
> 

On Tue, 2026-01-20 at 16:38 -0300, Wander Lairson Costa wrote:
> On Tue, Jan 20, 2026 at 01:30:35PM +0100, Gabriele Monaco wrote:
> 
> > You basically want i to be the length of the longest prefix common to at
> > least
> > another atom.
> > 
> > You could assign i to some python trick doing the exact same thing the loop
> > does, like:
> > 
> >     i = next((i for i in range(len(atom), -1, -1)
> >         if sum(a.startswith(atom[:i]) for a in atoms) > 1))
> > 
> > next() is basically doing the break at the first occurrence from the
> > generator,
> > just now your i doesn't live (only) inside the loop.
> > 
> > So now you save 2 lines and get any C developer scratch their head when they
> > look at the code, but hey, pyright is happy!
> > 
> 
> Or just leave the assignment.
> 
> > If you do find the trick with next() readable or have any better idea, feel
> > free
> > to try though.
> > 
> 
> Definitely the next() trick is not worth to make pyright happy.

Alright, thinking on this again next() is the python way to do if(...) break ,
it looked a bit odd to me only because I didn't know about it, but if you're
using python iterators, it kinda makes sense.

Anyway I'm fine also with the dull assignment, there's no need to argue on this.

Thanks,
Gabriele

> 
> > Thanks,
> > Gabriele
> > 
> > > I will modify it in v2.
> > > 
> > > > 
> > > > Thanks,
> > > > Gabriele
> > > > 
> > > > [1] - https://github.com/microsoft/pyright/issues/844
> > > > 
> > > > > 
> > > > > Signed-off-by: Wander Lairson Costa <wander@redhat.com>
> > > > > ---
> > > > >  tools/verification/rvgen/rvgen/ltl2k.py | 1 +
> > > > >  1 file changed, 1 insertion(+)
> > > > > 
> > > > > diff --git a/tools/verification/rvgen/rvgen/ltl2k.py
> > > > > b/tools/verification/rvgen/rvgen/ltl2k.py
> > > > > index fa9ea6d597095..94dc64af1716d 100644
> > > > > --- a/tools/verification/rvgen/rvgen/ltl2k.py
> > > > > +++ b/tools/verification/rvgen/rvgen/ltl2k.py
> > > > > @@ -45,6 +45,7 @@ def abbreviate_atoms(atoms: list[str]) -> list[str]:
> > > > >  
> > > > >      abbrs = []
> > > > >      for atom in atoms:
> > > > > +        i = 0
> > > > >          for i in range(len(atom), -1, -1):
> > > > >              if sum(a.startswith(atom[:i]) for a in atoms) > 1:
> > > > >                  break
> > > > 
> >