On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote: > Fix incorrect boolean logic in automata DOT file format validation > that allowed malformed files to pass undetected. The previous > implementation used a logical AND operator where OR was required, > causing the validation to only reject files when both the first > token was not "digraph" AND the second token was not > "state_automaton". This meant a file starting with "digraph" but > having an incorrect second token would incorrectly pass validation. > > The corrected logic properly rejects DOT files where either the > first token is not "digraph" or the second token is not > "state_automaton", ensuring that only properly formatted automaton > definition files are accepted for processing. Without this fix, > invalid DOT files could cause downstream parsing failures or > generate incorrect C code for runtime verification monitors. > > Signed-off-by: Wander Lairson Costa <[email protected]>
Right, that slipped. Thanks! Reviewed-by: Gabriele Monaco <[email protected]> > --- > tools/verification/rvgen/rvgen/automata.py | 2 +- > 1 file changed, 1 insertion(+), 1 deletion(-) > > diff --git a/tools/verification/rvgen/rvgen/automata.py > b/tools/verification/rvgen/rvgen/automata.py > index 9e1c097ad0e4a..7841a6e70bad2 100644 > --- a/tools/verification/rvgen/rvgen/automata.py > +++ b/tools/verification/rvgen/rvgen/automata.py > @@ -59,7 +59,7 @@ class Automata: > # checking the first line: > line = dot_lines[cursor].split() > > - if (line[0] != "digraph") and (line[1] != "state_automaton"): > + if (line[0] != "digraph") or (line[1] != "state_automaton"): > raise AutomataError(f"Not a valid .dot format: > {self.__dot_path}") > else: > cursor += 1
