Skip to content

Commit

Permalink
Support XML files containing failed results but no goto_trace field.
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
AmPaschal committed Dec 4, 2024
1 parent f68bb68 commit ca32113
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion src/cbmc_viewer/tracet.py
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit ca32113

Please sign in to comment.