[PATCH 0/2] verification/rvgen: Fix variable definition generation

From: Nam Cao
Date: Fri Jul 18 2025 - 10:58:33 EST


Hi,

The ltl2k script generates a variable definition for each node in the
abstract syntax tree. This may causes compiler warning on the generated
monitors, because:
- Some of the variables may be unused
- Some of the variables may be duplicated

This series fixes these issues.

Nam Cao (2):
verification/rvgen: Generate each variable definition only once
verification/rvgen: Do not generate unused variables

tools/verification/rvgen/rvgen/ltl2k.py | 33 +++++++++++++++++++------
1 file changed, 26 insertions(+), 7 deletions(-)

--
2.39.5