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

cbmc-viewer reports wrong count of successul proofs #152

Closed rod-chapman closed 3 weeks ago

rod-chapman commented 3 weeks ago

Re-running the verification of mlkem-c-aarch64 using the new CBMC 6.0.0 release, using the "run-cbmc-proofs.py" scripts, the output ends with:

| Status  | Count |
|---------|-------|
| Success | 7     |

| Proof                  | Status  |
|------------------------|---------|
| poly_compress          | Success |
| poly_decompress        | Success |
| scalar_compress_q_16   | Success |
| scalar_compress_q_32   | Success |
| scalar_decompress_q_16 | Success |
| scalar_decompress_q_32 | Success |

It says "7" Successes, but then only lists 6 functions in the table below. I have seen the same discrepency in the proof of s2n-tls. Is this a bug?

rod-chapman commented 3 weeks ago

If I deliberately break one of the proofs so it fails, then I get

## Summary of CBMC proof results

| Status  | Count |
|---------|-------|
| Fail    | 2     |
| Success | 5     |

| Proof                  | Status  |
|------------------------|---------|
| scalar_compress_q_16   | Fail    |
| scalar_decompress_q_16 | Fail    |
| poly_compress          | Success |
| poly_decompress        | Success |
| scalar_compress_q_32   | Success |
| scalar_decompress_q_32 | Success |

The "Success" count is always 1 too large.

tautschnig commented 3 weeks ago

Fixed in https://github.com/aws/s2n-tls/pull/4627 and https://github.com/model-checking/cbmc-starter-kit/pull/207.