replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
6,396 Commits 178 Branches 119 Tags 436 MiB
C++ 75.8%
C 12.9%
Java 3.2%
Scilab 1.8%
Objective-J 1.7%
Other 4.4%
Go to file
Michael Tautschnig ad24b5a9b9 Permit preprocessor command within __attribute__ 2016-04-12 12:29:00 +02:00
doc fixed bounds example 2016-04-07 13:03:39 +01:00
regression Permit preprocessor command within __attribute__ 2016-04-12 12:29:00 +02:00
scripts Move to latest git version of MiniSat as Debian no longer 2016-03-08 17:15:20 +00:00
src Permit preprocessor command within __attribute__ 2016-04-12 12:29:00 +02:00
unit Moved unit tests to separate directory 2016-02-16 13:00:54 +00:00
.travis.yml Initial README.md, including Travis-CI configuration 2016-03-19 12:16:25 +00:00
CHANGELOG added floating-point overflow checks 2014-01-28 14:51:27 +00:00
CODING_STANDARD initial commit 2011-05-08 12:26:13 +00:00
COMPILING we now use GIT; remove references to the SVN 2016-04-02 17:18:30 +01:00
LICENSE Daniel's affiliation 2014-08-28 12:09:54 +00:00
README.md fixed travis links in README.md 2016-03-20 23:27:33 +00:00

README.md

Build Status

CProver Wiki

About

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 also supports SystemC using Scoot. 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.

For full information see cprover.org.

License

4-clause BSD license, see LICENSE file.