Skip to content

Commit 8bd3903

Browse files
committed
CBMC: Add a link to list of undefined behaviors caught by CBMC
This commit adds a link to the list of undefined behaviors caught by CBMC to the CBMC README. Unfortunately, the HTML page targetted by the link is not rendered, limiting its usefulness. The CBMC team is aware, and we can update the link once there is a rendered version. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
1 parent cdeff27 commit 8bd3903

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)