Skip to content

Commit 8dba13b

Browse files
authored
Merge pull request #904 from pq-code-package/cbmc_note
CBMC: Add a link to list of undefined behaviors caught by CBMC
2 parents cdeff27 + 8bd3903 commit 8dba13b

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

proofs/cbmc/README.md

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -62,3 +62,5 @@ tests cbmc --help
6262
## What is covered?
6363
6464
Each proved function has an eponymous sub-directory of its own. Use [list_proofs.sh](list_proofs.sh) to see the list of functions covered.
65+
66+
The classes of undefined behavior covered by CBMC are documented [here](https://github.com/diffblue/cbmc/blob/develop/doc/C/c11-undefined-behavior.html).

0 commit comments

Comments
 (0)