Hi, 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, 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 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 devel/cbmc Content of the archive: devel/cbmc devel/cbmc/Makefile devel/cbmc/patches devel/cbmc/patches/patch-Makefiles devel/cbmc/patches/patch-bigint-fix-includes devel/cbmc/distinfo devel/cbmc/pkg devel/cbmc/pkg/PLIST devel/cbmc/pkg/DESCR BR Simon
Description: GNU Zip compressed data