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

Get AttributeError when running report for aws_hash_table_remove #23

Closed feliperodri closed 3 years ago

feliperodri commented 3 years ago

I get the following error message:

Traceback (most recent call last):
  File "/usr/local/bin/cbmc-viewer", line 11, in <module>
    sys.exit(viewer())
  File "/usr/local/lib/python3.6/dist-packages/cbmc_viewer/viewer.py", line 156, in viewer
    results = resultt.do_make_result(args.viewer_result, args.result)
  File "/usr/local/lib/python3.6/dist-packages/cbmc_viewer/resultt.py", line 438, in do_make_result
    return ResultFromCbmcXml(cbmc_result)
  File "/usr/local/lib/python3.6/dist-packages/cbmc_viewer/resultt.py", line 363, in __init__
    [self.parse_results(xml_file) for xml_file in xml_files]
  File "/usr/local/lib/python3.6/dist-packages/cbmc_viewer/resultt.py", line 76, in __init__
    [results[PROVER] for results in results_list]
  File "/usr/local/lib/python3.6/dist-packages/cbmc_viewer/resultt.py", line 166, in flatten_prover_list
    results = {result.lower() for result in prover_list}
  File "/usr/local/lib/python3.6/dist-packages/cbmc_viewer/resultt.py", line 166, in <setcomp>
    results = {result.lower() for result in prover_list}
AttributeError: 'NoneType' object has no attribute 'lower'

When running the proof verification/cbmc/proofs/aws_hash_table_remove in AWS C Common branch. Use make report2 to run the proof.

feliperodri commented 3 years ago

The verification failed with an Out of Memory message.

feliperodri commented 3 years ago

<message type="STATUS-MESSAGE">
  <text>converting SSA</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Running propositional reduction</text>
</message>

<message type="STATUS-MESSAGE">
  <text>Post-processing</text>
</message>

<message type="ERROR">
  <text>Out of memory</text>
</message>
markrtuttle commented 3 years ago

Is this an issue with viewer or an issue with cbmc running out of memory?

feliperodri commented 3 years ago

This issue has been fixed. Thank you @markrtuttle