File tree 1 file changed +21
-0
lines changed
1 file changed +21
-0
lines changed Original file line number Diff line number Diff line change
1
+ [ ![ Build Status] [ build_img ]] [ travis ]
2
+
3
+ About
4
+ =====
5
+
6
+ CBMC is a Bounded Model Checker for C and C++ programs. It supports C89, C99,
7
+ most of C11 and most compiler extensions provided by gcc and Visual Studio. It
8
+ also supports SystemC using Scoot. It allows verifying array bounds (buffer
9
+ overflows), pointer safety, exceptions and user-specified assertions.
10
+ Furthermore, it can check C and C++ for consistency with other languages, such
11
+ as Verilog. The verification is performed by unwinding the loops in the program
12
+ and passing the resulting equation to a decision procedure.
13
+
14
+ For full information see [ cprover.org] ( http://www.cprover.org/cbmc ) .
15
+
16
+ License
17
+ =======
18
+ 4-clause BSD license, see ` LICENSE ` file.
19
+
20
+ [ build_img ] : https://travis-ci.org/tautschnig/cbmc.svg?branch=master
21
+ [ travis ] : https://travis-ci.org/tautschnig/cbmc
You can’t perform that action at this time.
0 commit comments