Skip to content

Viewer Crashes when selected coverage is different from location e.g mcdc or branch #137

Open
@FlorianBarrau

Description

@FlorianBarrau

Description

CBMC Viewer crashes if we generate mcdc, branch, or decision coverage. In this issue we detail the mcdc trace problem. But this can be reproduced with other kind of coverage : branch, decision etc...

CBMC Viewer Version : 3.6
CBMC Version : 5.72.2
Ubuntu 18.04
GCC 7.5

How to reproduce

  1. Take the example from the README
  2. Replace coverage by mcdc for example
goto-cc -o main.goto main.c
cbmc main.goto --trace --xml-ui > result.xml
cbmc main.goto --cover mcdc --xml-ui > coverage.xml
cbmc main.goto --show-properties --xml-ui > property.xml
cbmc-viewer --goto main.goto --result result.xml --coverage coverage.xml --property property.xml --srcdir .
  1. CBMC Viewer trace
Traceback (most recent call last):
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 506, in parse_description
    basic_block = re.match(r'block [0-9]+ \(lines (.*)\)', description).group(1)
AttributeError: 'NoneType' object has no attribute 'group'

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

Traceback (most recent call last):
  File "/data/home/fb/.local/bin/cbmc-viewer", line 11, in <module>
    sys.exit(main())
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/cbmc_viewer.py", line 13, in main
    args.func(args)
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/viewer.py", line 98, in viewer
    coverage = coveraget.make_and_save_coverage(args, jsondir / 'viewer-coverage.json')
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 616, in make_and_save_coverage
    obj = make_coverage(args)
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 605, in make_coverage
    return CoverageFromCbmcXml(cbmc_coverage, srcdir)
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 390, in __init__
    [load_cbmc_xml(xml_file, root) for xml_file in xml_files]
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 390, in <listcomp>
    [load_cbmc_xml(xml_file, root) for xml_file in xml_files]
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 403, in load_cbmc_xml
    parse_description(goal.get("description")))
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 525, in parse_description
    raise UserWarning(f'Unexpected coverage goal description: "{description}"') from error
UserWarning: Unexpected coverage goal description: "decision/condition 'global > 0' false"

Other traces for different kind of coverage

  1. Decision
Traceback (most recent call last):
  File "/data/home/f00494530/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 506, in parse_description
    basic_block = re.match(r'block [0-9]+ \(lines (.*)\)', description).group(1)
AttributeError: 'NoneType' object has no attribute 'group'

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

Traceback (most recent call last):
  File "/data/home/fb/.local/bin/cbmc-viewer", line 11, in <module>
    sys.exit(main())
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/cbmc_viewer.py", line 13, in main
    args.func(args)
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/viewer.py", line 98, in viewer
    coverage = coveraget.make_and_save_coverage(args, jsondir / 'viewer-coverage.json')
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 616, in make_and_save_coverage
    obj = make_coverage(args)
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 605, in make_coverage
    return CoverageFromCbmcXml(cbmc_coverage, srcdir)
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 390, in __init__
    [load_cbmc_xml(xml_file, root) for xml_file in xml_files]
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 390, in <listcomp>
    [load_cbmc_xml(xml_file, root) for xml_file in xml_files]
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 403, in load_cbmc_xml
    parse_description(goal.get("description")))
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 525, in parse_description
    raise UserWarning(f'Unexpected coverage goal description: "{description}"') from error
UserWarning: Unexpected coverage goal description: "decision 'global > 0' false"
  1. Branch
Traceback (most recent call last):
  File "/data/home/f00494530/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 506, in parse_description
    basic_block = re.match(r'block [0-9]+ \(lines (.*)\)', description).group(1)
AttributeError: 'NoneType' object has no attribute 'group'

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

Traceback (most recent call last):
  File "/data/home/fb/.local/bin/cbmc-viewer", line 11, in <module>
    sys.exit(main())
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/cbmc_viewer.py", line 13, in main
    args.func(args)
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/viewer.py", line 98, in viewer
    coverage = coveraget.make_and_save_coverage(args, jsondir / 'viewer-coverage.json')
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 616, in make_and_save_coverage
    obj = make_coverage(args)
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 605, in make_coverage
    return CoverageFromCbmcXml(cbmc_coverage, srcdir)
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 390, in __init__
    [load_cbmc_xml(xml_file, root) for xml_file in xml_files]
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 390, in <listcomp>
    [load_cbmc_xml(xml_file, root) for xml_file in xml_files]
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 403, in load_cbmc_xml
    parse_description(goal.get("description")))
  File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 525, in parse_description
    raise UserWarning(f'Unexpected coverage goal description: "{description}"') from error
UserWarning: Unexpected coverage goal description: "entry point"

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't working

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions