Skip to content

Commit 324ed4d

Browse files
AmPaschaltautschnig
authored andcommitted
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.
1 parent b66d987 commit 324ed4d

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

src/cbmc_viewer/tracet.py

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -331,7 +331,9 @@ def parse_xml_traces(xmlfile, root=None):
331331
name, status = line.get('property'), line.get('status')
332332
if status == 'SUCCESS' or status == 'UNKNOWN':
333333
continue
334-
traces[name] = parse_xml_trace(line.find('goto_trace'), root)
334+
trace = line.find('goto_trace')
335+
if trace is not None:
336+
traces[name] = parse_xml_trace(trace, root)
335337
return traces
336338

337339
# cbmc produced only a one trace after being run with --stop-on-fail

0 commit comments

Comments
 (0)