first, nice port. I would like to test my own code with it. But you
missed the clang dependency. Your port is new and don't need a
Revision number of the current package. Defaults to empty (very
Why do you not fixed the missing RCS tags of the portscheck you made?
Little nitpick: as far as I know its more common to use spaces between
variables and their equals signs like in
## Entering big-int
gmake -C big-int
gmake: Entering directory
clang++ -c -MMD -MP -std=c++11 -Wall -O2 -o bigint-func.o
gmake: clang++: Command not found
gmake: *** [../common:183: bigint-func.o] Error 127
gmake: Leaving directory
gmake: *** [Makefile:50: big-int.dir] Error 2
*** Error 2 in . (/usr/ports/infrastructure/mk/bsd.port.mk:2671
*** Error 1 in . (/usr/ports/infrastructure/mk/bsd.port.mk:1884
*** Error 1 in . (/usr/ports/infrastructure/mk/bsd.port.mk:2409
*** Error 1 in . (/usr/ports/infrastructure/mk/bsd.port.mk:2389
*** Error 1 in . (/usr/ports/infrastructure/mk/bsd.port.mk:1901
*** Error 1 in /usr/ports/devel/cbmc
On Fri, Oct 14, 2016 at 08:15:21PM +0200, Simon Mages wrote:
> 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
> 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: