Skip to content

RMC script crash on --visualize and --unwinding-assertions #199

@avanhatt

Description

@avanhatt

Can we generate any useful visualizations with --unwinding-assertions, even without coverage info? Or can we at least give a more clear error message?

rmc (main-152-2021-06-07) $ rmc --visualize src/test/cbmc/DynTrait/main.rs --unwinding-assertions
<?xml version="1.0" encoding="UTF-8"?>
<cprover>
<program>CBMC 5.31.0 (cbmc-5.31.0)</program>
<message type="ERROR">
  <text>--cover and --unwinding-assertions must not be given together</text>
</message>


Traceback (most recent call last):
  File "/usr/local/bin/cbmc-viewer", line 10, in <module>
    sys.exit(viewer())
  File "/Library/Python/3.8/site-packages/cbmc_viewer/viewer.py", line 167, in viewer
    coverage = coveraget.do_make_coverage(args.viewer_coverage,
  File "/Library/Python/3.8/site-packages/cbmc_viewer/coveraget.py", line 551, in do_make_coverage
    return CoverageFromCbmcXml(cbmc_coverage, srcdir)
  File "/Library/Python/3.8/site-packages/cbmc_viewer/coveraget.py", line 392, in __init__
    [load_cbmc_xml(xml_file, root) for xml_file in xml_files]
  File "/Library/Python/3.8/site-packages/cbmc_viewer/coveraget.py", line 392, in <listcomp>
    [load_cbmc_xml(xml_file, root) for xml_file in xml_files]
  File "/Library/Python/3.8/site-packages/cbmc_viewer/coveraget.py", line 398, in load_cbmc_xml
    xml = parse.parse_xml_file(xml_file, fail=True)
  File "/Library/Python/3.8/site-packages/cbmc_viewer/parse.py", line 17, in parse_xml_file
    return parse_xml_string(data.read(), xfile, fail)
  File "/Library/Python/3.8/site-packages/cbmc_viewer/parse.py", line 46, in parse_xml_string
    raise UserWarning(message) from None
UserWarning: Can't parse xml file coverage.xml: string <?xml version="1.0" encoding="UTF-8"?>
<...: no element found: line 8, column 0

Metadata

Metadata

Assignees

Labels

[C] BugThis is a bug. Something isn't working.

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions