cbmc-viewer icon indicating copy to clipboard operation
cbmc-viewer copied to clipboard

Support XML files containing failed results but no goto_trace field.

Open AmPaschal opened this issue 11 months ago • 0 comments

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

CBMC 6.3.1 (cbmc-6.3.1) CBMC version 6.3.1 (cbmc-6.3.1) 64-bit x86_64 linux

...

Running SMT2 ALL (with FPA) using CVC5 Runtime Solver: 0.00640582s Runtime decision procedure: 0.00703132s VERIFICATION ERROR

ERROR

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

AmPaschal avatar Dec 04 '24 19:12 AmPaschal