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

Viewer crashes when building report for proofs with contracts #134

Closed feliperodri closed 1 year ago

feliperodri commented 1 year ago

Version: 3.6

Reproduce: coreJSON. 

Traceback (most recent call last):

  File "/usr/local/Cellar/cbmc-viewer/3.6/libexec/lib/python3.8/site-packages/cbmc_viewer/coveraget.py", line 543, in parse_basic_block_lines

    assert all(fyle and func and line for fyle, func, line in lines)

AssertionError

The above exception was the direct cause of the following exception:

Traceback (most recent call last):

  File "/usr/local/bin/cbmc-viewer", line 8, in <module>

    sys.exit(main())

  File "/usr/local/Cellar/cbmc-viewer/3.6/libexec/lib/python3.8/site-packages/cbmc_viewer/cbmc_viewer.py", line 13, in main

    args.func(args)

  File "/usr/local/Cellar/cbmc-viewer/3.6/libexec/lib/python3.8/site-packages/cbmc_viewer/viewer.py", line 98, in viewer

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

  File "/usr/local/Cellar/cbmc-viewer/3.6/libexec/lib/python3.8/site-packages/cbmc_viewer/coveraget.py", line 616, in make_and_save_coverage

    obj = make_coverage(args)

  File "/usr/local/Cellar/cbmc-viewer/3.6/libexec/lib/python3.8/site-packages/cbmc_viewer/coveraget.py", line 605, in make_coverage

    return CoverageFromCbmcXml(cbmc_coverage, srcdir)

  File "/usr/local/Cellar/cbmc-viewer/3.6/libexec/lib/python3.8/site-packages/cbmc_viewer/coveraget.py", line 390, in __init__

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

  File "/usr/local/Cellar/cbmc-viewer/3.6/libexec/lib/python3.8/site-packages/cbmc_viewer/coveraget.py", line 390, in <listcomp>

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

  File "/usr/local/Cellar/cbmc-viewer/3.6/libexec/lib/python3.8/site-packages/cbmc_viewer/coveraget.py", line 402, in load_cbmc_xml

    lines = (parse_basic_block_lines(goal.find("basic_block_lines")) or

  File "/usr/local/Cellar/cbmc-viewer/3.6/libexec/lib/python3.8/site-packages/cbmc_viewer/coveraget.py", line 547, in parse_basic_block_lines

    raise UserWarning(f'Unexpected coverage goal xml data: "{basic_block_lines}"') from error

UserWarning: Unexpected coverage goal xml data: "<Element 'basic_block_lines' at 0x1070cb720>"

ninja: build stopped: cannot make progress due to previous errors.
jimgrundy commented 1 year ago

It becomes a gating issues for deploying contracts if viewer crashes given the starter-kit dependence on it. I don't mind if it produces results that don't help in understanding a trace. I don't mind if is screams with a bunch of warnings (in fact, I'd rather like that), but we need it terminate correctly.