__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 <[email protected]>
Signed-off-by: Gabriele Monaco <[email protected]>
---
tools/verification/rvgen/rvgen/dot2k.py | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py
b/tools/verification/rvgen/rvgen/dot2k.py
index e6f476b90..110cfd69e 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)"
--
2.54.0
