cbmc-viewer
cbmc-viewer copied to clipboard
Support XML files containing failed results but no goto_trace field.
Issue #, if available:
Description of changes: 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.
Here is a sample XML file that triggers this crash
...
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.