Hi Simon,

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
        first package),...

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[1]: Entering directory
clang++ -c -MMD -MP -std=c++11  -Wall -O2  -o bigint-func.o
gmake[1]: clang++: Command not found
gmake[1]: *** [../common:183: bigint-func.o] Error 127
gmake[1]: 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
(/usr/ports/infrastructure/mk/bsd.port.mk:2389 'install')

On Fri, Oct 14, 2016 at 08:15:21PM +0200, Simon Mages wrote:
> 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, 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
> 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

Reply via email to