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.

bsd,port.mk(5):
REVISION
        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
/usr/ports/infrastructure/templates/Makefile.template.

bye,
Jan

log:

## Entering big-int
gmake  -C big-int
gmake[1]: Entering directory
'/usr/ports/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/big-int'
clang++ -c -MMD -MP -std=c++11  -Wall -O2  -o bigint-func.o
bigint-func.cc
gmake[1]: clang++: Command not found
gmake[1]: *** [../common:183: bigint-func.o] Error 127
gmake[1]: Leaving directory
'/usr/ports/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/big-int'
gmake: *** [Makefile:50: big-int.dir] Error 2
*** Error 2 in . (/usr/ports/infrastructure/mk/bsd.port.mk:2671
'/usr/ports/pobj/cbmc-5.5/.build_done')
*** Error 1 in . (/usr/ports/infrastructure/mk/bsd.port.mk:1884
'/usr/ports/packages/amd64/all/cbmc-5.5p0.tgz')
*** Error 1 in . (/usr/ports/infrastructure/mk/bsd.port.mk:2409
'_internal-package')
*** Error 1 in . (/usr/ports/infrastructure/mk/bsd.port.mk:2389
'package')
*** Error 1 in . (/usr/ports/infrastructure/mk/bsd.port.mk:1901
'/var/db/pkg/cbmc-5.5p0/+CONTENTS')
*** 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