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 selected coverage is different from `location` e.g `mcdc` or `branch` #137

Open FlorianBarrau opened 1 year ago

FlorianBarrau commented 1 year ago

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 .
  3. 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 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 [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
```bash
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 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 [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"