[PATCH v2 07/14] verification/rvgen: Fix ltl2k writing True as a literal
flat view
STALE132d
LANDED
From: Gabriele Monaco <gmonaco@redhat.com>
Date: 2026-05-14 15:21:47
Also in:
lkml
Subsystem:
runtime verification (rv), the rest · Maintainers:
Steven Rostedt, Gabriele Monaco, Linus Torvalds
Revision v2 of 5 in this series; landed in mainline as df996599cc69 on 2026-06-04.
Revisions (5)
The rvgen parser for LTL stores literal true values in the python
representation (capitalised True), this doesn't build in C.
The Literal class should already handle this case but ASTNode skips its
strigification method and converts the value (true/false) directly.
Fix by delegating ASTNode stringification to the Literal and Variable
classes instead of bypassing them.
Fixes: 97ffa4ce6ab32 ("verification/rvgen: Add support for linear temporal logic")
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
---
tools/verification/rvgen/rvgen/ltl2ba.py | 9 +++++----
1 file changed, 5 insertions(+), 4 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
index 7f538598a868..016e7cf93bbb 100644
--- a/tools/verification/rvgen/rvgen/ltl2ba.py
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py@@ -122,10 +122,8 @@ class ASTNode: return self.op.expand(self, node, node_set) def __str__(self): - if isinstance(self.op, Literal): - return str(self.op.value) - if isinstance(self.op, Variable): - return self.op.name.lower() + if isinstance(self.op, (Literal, Variable)): + return str(self.op) return "val" + str(self.id) def normalize(self):
@@ -382,6 +380,9 @@ class Variable: def __iter__(self): yield from () + def __str__(self): + return self.name.lower() + def negate(self): new = ASTNode(self) return NotOp(new)
--
2.54.0