search

model-checking / cbmc-viewer

CBMC Viewer scans the output of CBMC and produces a browsable summary of its findings, making it easy to root cause the issues it finds.
https://model-checking.github.io/cbmc-viewer/
Apache License 2.0
32 stars 11 forks source link

Crashes when using CBMC 6 #148

Closed adpaco-aws closed 3 weeks ago

adpaco-aws commented 7 months ago

CBMC version 6 includes at least one breaking change which was noticeable when the CI system in the s2n-tls repo picked it up as a pre-release version in this run. The error coming from cbmc-viewer is:

 Traceback (most recent call last):
  File "/home/runner/.local/bin/cbmc-viewer", line 8, in <module>

    sys.exit(main())

  File "/home/runner/.local/lib/python3.10/site-packages/cbmc_viewer/cbmc_viewer.py", line 13, in main

    args.func(args)

  File "/home/runner/.local/lib/python3.10/site-packages/cbmc_viewer/viewer.py", line 98, in viewer

    coverage = coveraget.make_and_save_coverage(args, jsondir / 'viewer-coverage.json')

  File "/home/runner/.local/lib/python3.10/site-packages/cbmc_viewer/coveraget.py", line 667, in make_and_save_coverage

    obj = make_coverage(args)

  File "/home/runner/.local/lib/python3.10/site-packages/cbmc_viewer/coveraget.py", line 656, in make_coverage

    return CoverageFromCbmcXml(cbmc_coverage, srcdir)

  File "/home/runner/.local/lib/python3.10/site-packages/cbmc_viewer/coveraget.py", line 419, in __init__

    [load_cbmc_xml(xml_file, root) for xml_file in xml_files]

  File "/home/runner/.local/lib/python3.10/site-packages/cbmc_viewer/coveraget.py", line 419, in <listcomp>

    [load_cbmc_xml(xml_file, root) for xml_file in xml_files]

  File "/home/runner/.local/lib/python3.10/site-packages/cbmc_viewer/coveraget.py", line 433, in load_cbmc_xml

    parse_description(goal.get("description")))

  File "/home/runner/.local/lib/python3.10/site-packages/cbmc_viewer/coveraget.py", line 543, in parse_description

    basic_block = re.match(r'block [0-9]+ \(lines (.*)\)', description).group(1)

AttributeError: 'NoneType' object has no attribute 'group'

The error points to an issue when parsing descriptions from basic block information in XML files. We need to investigate further.

tautschnig commented 3 weeks ago

I have not seen this anymore in more recent uses of cbmc-viewer with CBMC v6. Closing, but should be re-opened in case we run into this again.