diff options
| author | Gabriele Monaco <gmonaco@redhat.com> | 2026-06-01 17:38:38 +0200 |
|---|---|---|
| committer | Gabriele Monaco <gmonaco@redhat.com> | 2026-06-04 16:44:25 +0200 |
| commit | 85339442de941e4d7ff5d53f51ae1413905e45ec (patch) | |
| tree | 8d1dde8a2b817c3c5e629e5daad735d996114f7c /tools/verification | |
| parent | 33ec2269a4155cad7e9e42c92327dcaa9aee59a7 (diff) | |
verification/rvgen: Fix suffix strip in dot2k
__start_to_invariant_check() and __get_constraint_env() parse the
environment variable's name from sources that have it padded with the
monitor name. This is removed using rstrip(), which is not meant to
strip a substring but rather a set of characters.
Use removesuffix() to actually get rid of the trailing _<monitor name>.
Fixes: a82adadb16894 ("verification/rvgen: Add support for Hybrid Automata")
Reviewed-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20260601153840.124372-12-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
Diffstat (limited to 'tools/verification')
| -rw-r--r-- | tools/verification/rvgen/rvgen/dot2k.py | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py index e6f476b903b0..110cfd69e53a 100644 --- a/tools/verification/rvgen/rvgen/dot2k.py +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -215,14 +215,14 @@ class ha2k(dot2k): def __get_constraint_env(self, constr: str) -> str: """Extract the second argument from an ha_ function""" env = constr.split("(")[1].split()[1].rstrip(")").rstrip(",") - assert env.rstrip(f"_{self.name}") in self.envs + assert env.removesuffix(f"_{self.name}") in self.envs return env def __start_to_invariant_check(self, constr: str) -> str: # by default assume the timer has ns expiration env = self.__get_constraint_env(constr) clock_type = "ns" - if self.env_types.get(env.rstrip(f"_{self.name}")) == "j": + if self.env_types.get(env.removesuffix(f"_{self.name}")) == "j": clock_type = "jiffy" return f"return ha_check_invariant_{clock_type}(ha_mon, {env}, time_ns)" |