Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
FlorianBarrau opened this issue Dec 15, 2022 · 0 comments
Labels
bug Something isn't working

Comments

@FlorianBarrau
Copy link

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"
@feliperodri feliperodri added the bug Something isn't working label Jul 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

2 participants