forked from Lainports/freebsd-ports
7f087b720e
Bounded Model Checker for C and C++ programs https://github.com/diffblue/cbmc Sponsored by: Netflix
7 lines
484 B
Text
7 lines
484 B
Text
CBMC is a Bounded Model Checker for C and C++ programs.
|
|
It supports C89, C99, most of C11 and most compiler extensions provided by gcc
|
|
and Visual Studio. It allows verifying array bounds (buffer overflows), pointer
|
|
safety, exceptions and user-specified assertions. Furthermore, it can check C
|
|
and C++ for consistency with other languages, such as Verilog.
|
|
The verification is performed by unwinding the loops in the program and passing
|
|
the resulting equation to a decision procedure.
|