replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
8,244 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
Daniel Kroening eb93231018 Merge pull request #526 from martin-cs/fix-cfg-dominator-top 
Fix cfg dominator top
 		2017-03-13 15:26:36 +00:00
.githooks Make the pre-commit hook report non-temporary path names (#477) 2017-02-02 20:39:09 +00:00
doc Normalise newlines at ends of files 2016-11-29 09:59:31 +00:00
regression Merge pull request #604 from mgudemann/limit_class_loading 2017-03-13 15:20:38 +00:00
scripts Merge pull request #558 from rjmunro/feature/cpplint-sed-format 2017-03-13 15:26:01 +00:00
src Merge pull request #526 from martin-cs/fix-cfg-dominator-top 2017-03-13 15:26:36 +00:00
unit miniBDD lint-cleaning: whitespace adjustments 2017-02-14 18:40:33 +00:00
.editorconfig Don't remove trailing spaces from patch files 2016-11-29 17:26:59 +00:00
.gitattributes added test.desc as text 2016-08-15 12:35:10 +01:00
.gitignore Additions to the gitignore 2017-02-03 10:42:59 +00:00
.travis.yml Merge pull request #541 from smowton/string-refine-unicode 2017-03-01 07:18:11 -05:00
CHANGELOG added floating-point overflow checks 2014-01-28 14:51:27 +00:00
CODING_STANDARD Merge pull request #415 from thk123/feature/lint-check-multi-line-function-call 2017-01-11 18:30:14 +00:00
COMPILING libzip/zlib download no longer needed 2017-03-07 19:30:12 -08:00
LICENSE update year 2016-09-05 17:05:55 +01: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.