Failure on readme example

[jkbbwr]

When using the instructions from the README.MD I get the following exception

CBMC Viewer 3.5

Traceback (most recent call last):
  File "/home/jakob/.local/lib/python3.10/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 "/usr/bin/cbmc-viewer", line 8, in <module>
    sys.exit(main())
  File "/home/jakob/.local/lib/python3.10/site-packages/cbmc_viewer/cbmc_viewer.py", line 13, in main
    args.func(args)
  File "/home/jakob/.local/lib/python3.10/site-packages/cbmc_viewer/viewer.py", line 98, in viewer
    coverage = coveraget.make_and_save_coverage(args, jsondir / 'viewer-coverage.json')
  File "/home/jakob/.local/lib/python3.10/site-packages/cbmc_viewer/coveraget.py", line 616, in make_and_save_coverage
    obj = make_coverage(args)
  File "/home/jakob/.local/lib/python3.10/site-packages/cbmc_viewer/coveraget.py", line 605, in make_coverage
    return CoverageFromCbmcXml(cbmc_coverage, srcdir)
  File "/home/jakob/.local/lib/python3.10/site-packages/cbmc_viewer/coveraget.py", line 390, in __init__
    [load_cbmc_xml(xml_file, root) for xml_file in xml_files]
  File "/home/jakob/.local/lib/python3.10/site-packages/cbmc_viewer/coveraget.py", line 390, in <listcomp>
    [load_cbmc_xml(xml_file, root) for xml_file in xml_files]
  File "/home/jakob/.local/lib/python3.10/site-packages/cbmc_viewer/coveraget.py", line 403, in load_cbmc_xml
    parse_description(goal.get("description")))
  File "/home/jakob/.local/lib/python3.10/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: "block 1"

[tautschnig]

It seems that CBMC produced output that we didn't expect here. CBMC had some issues here in the past, but we were hoping to have ironed these out. Would it be possible to share the source code where you ended up with this result to help us debug?

[jkbbwr]

https://gist.github.com/jkbbwr/d22fc3efcc01ffc4cd0a671fbdef904c

Here are all the XMLs produced. Is that enough?

[markrtuttle]

I can reproduce with

cbmc-viewer coverage --coverage coverage.xml --srcdir /home/jakob/tmp

[markrtuttle]

Can you provide the source file? Can you provide the output of cbmc --version?

[markrtuttle]

It looks like the version of cbmc that produced the coverage.xml file produced coverage goal blocks of the form

<goal description="block 1" id="main.coverage.1" status="SATISFIED">
  <location file="main.c" function="main" line="6" working-directory="/home/jakob/tmp"/>
</goal>

In contrast, cbmc 5.60 on the FreeRTOS kernel example produces

<goal description="block 16 (lines /private/tmp/kernel/portable/MemMang/heap_5.c:pvPortMalloc:246)" id="pvPortMalloc.coverage.16" status="FAILED">
  <location file="/private/tmp/kernel/portable/MemMang/heap_5.c" function="pvPortMalloc" line="246" working-directory="/private/tmp/kernel/cbmc/proofs/pvPortMalloc"/>
  <basic_block_lines>
    <line file="/private/tmp/kernel/portable/MemMang/heap_5.c" function="pvPortMalloc">246</line>
  </basic_block_lines>
</goal>

[tautschnig]

@jkbbwr It seems you are using version 5.11 of CBMC. Would you mind upgrading to a more recent version (latest is 5.60) as available from https://github.com/diffblue/cbmc/releases?

[jkbbwr]

Shall attempt and report back

[tautschnig]

@jkbbwr We'll assume this issue is fixed for you. Feel free to reopen if this isn't the case.