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: a82adadb16 ("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>
This commit is contained in:
Gabriele Monaco 2026-06-01 17:38:38 +02:00
parent 33ec2269a4
commit 85339442de

View File

@ -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)"