From ca32113f1c73b33867c72957c2b7f900d02236f0 Mon Sep 17 00:00:00 2001 From: Paschal Amusuo Date: Wed, 4 Dec 2024 14:54:37 -0500 Subject: [PATCH] Support XML files containing failed results but no goto_trace field. Some CBMC solvers like CVC5 can generate a cbmc.xml file containing failed verification results but without the failure trace (or a goto_trace field). With the current behavior, cbmc_viewer will crash when invoked because line 353 will try to iterate through None. This commit fixes this bug. --- src/cbmc_viewer/tracet.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/cbmc_viewer/tracet.py b/src/cbmc_viewer/tracet.py index 6bcd7d8..8c7bb9c 100644 --- a/src/cbmc_viewer/tracet.py +++ b/src/cbmc_viewer/tracet.py @@ -331,7 +331,9 @@ def parse_xml_traces(xmlfile, root=None): name, status = line.get('property'), line.get('status') if status == 'SUCCESS' or status == 'UNKNOWN': continue - traces[name] = parse_xml_trace(line.find('goto_trace'), root) + trace = line.find('goto_trace') + if trace is not None: + traces[name] = parse_xml_trace(trace, root) return traces # cbmc produced only a one trace after being run with --stop-on-fail