./devel/cbmc [Bounded Model Checker for C and C++ programs]
[+] Add this package to your ports tracker

[ 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)
  • (2016-10-23) Package added to openports.se, version cbmc-5.5 (created)
[show/hide] View available PLISTS (Can be a lot of data)

CVS Commit History:

   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