this is my first port, i hope everything is fine.

A college of mine was using this tool to analyse some C code. I think this
tool is pretty interesting and can be put to good use for all sorts of programs
or parts of it.

COMMENT=        Bounded Model Checker for C and C++ programs

# cat pkg/DESCR
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. We have recently added experimental support
for Java Bytecode.

CBMC verifies array bounds (buffer overflows), pointer safety, ex­cep­tions
and user-specified as­ser­tions. 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 re­sul­ting
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
since version 3.3. The solvers we recommend 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.

# portcheck
Makefile does not have $OpenBSD$ RCS tag at the top
patches/patch-Makefiles does not have $OpenBSD$ RCS tag at the top
patches/patch-bigint-fix-includes does not have $OpenBSD$ RCS tag at the top

Content of the archive:


Attachment: cbmc-5.5.tar.gz
Description: GNU Zip compressed data

Reply via email to