Re: [PATCH 17/26] rv/rvgen: fix possibly unbound variable in ltl2k

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:

quoted

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.

quoted

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

quoted

Thanks,
Gabriele

quoted

I will modify it in v2.

quoted

Thanks,
Gabriele

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

quoted

Signed-off-by: Wander Lairson Costa <redacted>
---
 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