replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
8,328 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
Lucas Cordeiro b4ae916056 Enabled test cases in goto-instrument after fixes in the full-slice 
Enabled test cases slice01, slice13, and slice16 in the goto-instrument regression
suite after fixes related to commits 27227cc and 211cb90.
 		2017-03-28 09:59:41 +01: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 Enabled test cases in goto-instrument after fixes in the full-slice 2017-03-28 09:59:41 +01:00
scripts Check that filter_lint_by_diff.py exists 2017-03-21 14:09:44 +00:00
src Merge pull request #681 from peterschrammel/no-assertions-for-user-only 2017-03-25 09:43:38 +00:00
unit map with sharing 2017-03-18 19:13:48 +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 Added IDE files to .gitignore 2017-03-14 10:20:06 +00:00
.travis.yml Add test for Alpine linux (musl-libc). 2017-03-10 12:03:46 +00:00
CHANGELOG Initial version of release notes for 5.7 2017-03-24 19:19:36 +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 Updates for GCC 6 2017-03-23 10:31:24 +00: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.