Navigation:
devel cbmc
CVSweb ] [ 
Homepage ] [ 
RSS feed ]| Version: 5.5, Package name: cbmc-5.5 |
| Maintained by: Mages Simon |
| Master sites: |
| Description 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, and has experimental support for Java Bytecode. CBMC verifies 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. While CBMC is aimed for embedded software, it also supports dynamic memory allocation using malloc and new. CBMC comes with a built-in solver for bit-vector formulas that is based on MiniSat. As an alternative, CBMC has featured support for external SMT solvers. Recommended solvers are (in no particular order) Boolector, MathSAT, Yices 2 and Z3. Note that these solvers need to be installed separately and have different licensing conditions. |
| Filesize: 43.192 KB |
| Version History (View Complete History) |
|
| 2021-11-28 05:45:46 by Stuart Henderson | Files touched by this commit (1) |
Log message: use correct GH_TAGNAME, use GH_DISTFILE |
| 2021-05-12 08:44:18 by Christian Weisgerber | Files touched by this commit (5) |
Log message: devel/cbmc: unbreak parallel build List the header files generated by bison as targets in Makefile rules since they are prerequisites in other rules. |
| 2021-05-09 07:27:14 by Todd C. Miller | Files touched by this commit (6) |
Log message: Use --defines=filename.h instead of -d to fix build with bison 3.7. The y.tab.c file equivalent now includes the generated header so it cannot simply be moved to a new name. OK sthen@ |
| 2019-07-12 14:44:13 by Stuart Henderson | Files touched by this commit (877) |
Log message: replace simple PERMIT_PACKAGE_CDROM=Yes with PERMIT_PACKAGE=Yes |
| 2017-07-26 16:45:35 by Stuart Henderson | Files touched by this commit (937) |
Log message: bump LIBCXX/LIBECXX/COMPILER_LIBCXX ports. |
| 2017-07-23 03:26:30 by Marc Espie | Files touched by this commit (244) |
Log message: add pthread to COMPILER_LIBCXX. white lie, but it allows clang and gcc to be more similar bump accordingly. |
| 2017-07-16 13:19:06 by Marc Espie | Files touched by this commit (880) |
Log message: use COMPILER_LIBCXX where applicable |
| 2017-05-31 02:08:18 by Marc Espie | Files touched by this commit (173) |
Log message: switch everything to new COMPILER idiom, even stuff that won't build with clang yet, but at least that part is done. |
| 2017-05-26 22:41:43 by Marc Espie | Files touched by this commit (4) |
Log message: use WANT_CXX, these build trivially |
| 2016-11-02 15:05:38 by Stuart Henderson | Files touched by this commit (1) |
Log message: fix WANTLIB, it was totally missing |