Commit f3735df6 authored by Nam Cao's avatar Nam Cao Committed by Steven Rostedt (Google)
Browse files

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.

Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Link: https://lore.kernel.org/636b2b2d99a9bd46a9f77a078d44ebd7ffc7508c.1752850449.git.namcao@linutronix.de


Signed-off-by: default avatarNam Cao <namcao@linutronix.de>
Reviewed-by: default avatarGabriele Monaco <gmonaco@redhat.com>
Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
parent 6fb37c2a

tools/verification/rvgen/rvgen/ltl2k.py

+21 −4
Original line number Diff line number Diff line
@@ -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: