diff options
Diffstat (limited to 'devel/cbmc/pkg-descr')
| -rw-r--r-- | devel/cbmc/pkg-descr | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/devel/cbmc/pkg-descr b/devel/cbmc/pkg-descr new file mode 100644 index 000000000000..2004194d7c43 --- /dev/null +++ b/devel/cbmc/pkg-descr @@ -0,0 +1,7 @@ +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. |