[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-Id: <636b2b2d99a9bd46a9f77a078d44ebd7ffc7508c.1752850449.git.namcao@linutronix.de>
Date: Fri, 18 Jul 2025 16:58:11 +0200
From: Nam Cao <namcao@...utronix.de>
To: Steven Rostedt <rostedt@...dmis.org>,
Masami Hiramatsu <mhiramat@...nel.org>,
Mathieu Desnoyers <mathieu.desnoyers@...icios.com>,
Gabriele Monaco <gmonaco@...hat.com>,
linux-trace-kernel@...r.kernel.org,
linux-kernel@...r.kernel.org
Cc: Nam Cao <namcao@...utronix.de>
Subject: [PATCH 2/2] verification/rvgen: Do not generate unused variables
ltl2k generates all variable definition in both ltl_start() and
ltl_possible_next_states(). However, these two functions may not use all
the variables, causing "unused variable" compiler warning.
Change the script to only generate used variables.
Signed-off-by: Nam Cao <namcao@...utronix.de>
---
tools/verification/rvgen/rvgen/ltl2k.py | 25 +++++++++++++++++++++----
1 file changed, 21 insertions(+), 4 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py
index 59da351792ec..b075f98d50c4 100644
--- a/tools/verification/rvgen/rvgen/ltl2k.py
+++ b/tools/verification/rvgen/rvgen/ltl2k.py
@@ -106,20 +106,25 @@ class ltl2k(generator.Monitor):
])
return buf
- def _fill_atom_values(self):
+ def _fill_atom_values(self, required_values):
buf = []
for node in self.ltl:
- if node.op.is_temporal():
+ if str(node) not in required_values:
continue
if isinstance(node.op, ltl2ba.AndOp):
buf.append("\tbool %s = %s && %s;" % (node, node.op.left, node.op.right))
+ required_values |= {str(node.op.left), str(node.op.right)}
elif isinstance(node.op, ltl2ba.OrOp):
buf.append("\tbool %s = %s || %s;" % (node, node.op.left, node.op.right))
+ required_values |= {str(node.op.left), str(node.op.right)}
elif isinstance(node.op, ltl2ba.NotOp):
buf.append("\tbool %s = !%s;" % (node, node.op.child))
+ required_values.add(str(node.op.child))
for atom in self.atoms:
+ if atom.lower() not in required_values:
+ continue
buf.append("\tbool %s = test_bit(LTL_%s, mon->atoms);" % (atom.lower(), atom))
buf.reverse()
@@ -135,7 +140,13 @@ class ltl2k(generator.Monitor):
"ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)",
"{"
]
- buf.extend(self._fill_atom_values())
+
+ required_values = set()
+ for node in self.ba:
+ for o in sorted(node.outgoing):
+ required_values |= o.labels
+
+ buf.extend(self._fill_atom_values(required_values))
buf.extend([
"",
"\tswitch (state) {"
@@ -166,7 +177,13 @@ class ltl2k(generator.Monitor):
"static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)",
"{"
]
- buf.extend(self._fill_atom_values())
+
+ required_values = set()
+ for node in self.ba:
+ if node.init:
+ required_values |= node.labels
+
+ buf.extend(self._fill_atom_values(required_values))
buf.append("")
for node in self.ba:
--
2.39.5
Powered by blists - more mailing lists