Linux Trace Kernel
 help / color / mirror / Atom feed
From: Gabriele Monaco <gmonaco@redhat.com>
To: linux-kernel@vger.kernel.org, linux-trace-kernel@vger.kernel.org,
	Steven Rostedt <rostedt@goodmis.org>,
	Gabriele Monaco <gmonaco@redhat.com>,
	Nam Cao <namcao@linutronix.de>
Cc: Thomas Weissschuh <thomas.weissschuh@linutronix.de>,
	Tomas Glozar <tglozar@redhat.com>, John Kacur <jkacur@redhat.com>,
	Wen Yang <wen.yang@linux.dev>
Subject: [PATCH v2 07/14] verification/rvgen: Fix ltl2k writing True as a literal
Date: Thu, 14 May 2026 17:20:48 +0200	[thread overview]
Message-ID: <20260514152055.229162-8-gmonaco@redhat.com> (raw)
In-Reply-To: <20260514152055.229162-1-gmonaco@redhat.com>

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


  parent reply	other threads:[~2026-05-14 15:21 UTC|newest]

Thread overview: 15+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2026-05-14 15:20 [PATCH v2 00/14] rv: Add selftests to tools and KUnit tests Gabriele Monaco
2026-05-14 15:20 ` [PATCH v2 01/14] tools/rv: Fix substring match bug in monitor name search Gabriele Monaco
2026-05-14 15:20 ` [PATCH v2 02/14] tools/rv: Fix substring match when listing container monitors Gabriele Monaco
2026-05-14 15:20 ` [PATCH v2 03/14] tools/rv: Fix exit status when monitor execution fails Gabriele Monaco
2026-05-14 15:20 ` [PATCH v2 04/14] tools/rv: Fix cleanup after failed trace setup Gabriele Monaco
2026-05-14 15:20 ` [PATCH v2 05/14] tools/rv: Add selftests Gabriele Monaco
2026-05-14 15:20 ` [PATCH v2 06/14] verification/rvgen: Fix options shared among commands Gabriele Monaco
2026-05-14 15:20 ` Gabriele Monaco [this message]
2026-05-14 15:20 ` [PATCH v2 08/14] verification/rvgen: Add golden and spec folders for tests Gabriele Monaco
2026-05-14 15:20 ` [PATCH v2 09/14] verification/rvgen: Add selftests Gabriele Monaco
2026-05-14 15:20 ` [PATCH v2 10/14] rv: Add KUnit stub to rv_react() and rv_*_task_monitor_slot() Gabriele Monaco
2026-05-14 15:20 ` [PATCH v2 11/14] rv: Add KUnit tests for some DA/HA monitors Gabriele Monaco
2026-05-14 15:20 ` [PATCH v2 12/14] rv: Add KUnit stubs for current and smp_processor_id() Gabriele Monaco
2026-05-14 15:20 ` [PATCH v2 13/14] rv: Prevent unintentional tracepoints during KUnit tests Gabriele Monaco
2026-05-14 15:20 ` [PATCH v2 14/14] rv: Add KUnit tests for some LTL monitors Gabriele Monaco

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20260514152055.229162-8-gmonaco@redhat.com \
    --to=gmonaco@redhat.com \
    --cc=jkacur@redhat.com \
    --cc=linux-kernel@vger.kernel.org \
    --cc=linux-trace-kernel@vger.kernel.org \
    --cc=namcao@linutronix.de \
    --cc=rostedt@goodmis.org \
    --cc=tglozar@redhat.com \
    --cc=thomas.weissschuh@linutronix.de \
    --cc=wen.yang@linux.dev \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox