Hi, Am Samstag, 15. Oktober 2016 schrieb Jan Klemkow :
> Hi Simon, > > first, nice port. I would like to test my own code with it. But you > missed the clang dependency. Well, i thought that a new port will not be taged for a past release. If this is wrong i can add the dependency. > Your port is new and don't need a > REVISION. Ok, will fix that. > 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? What should i fix there? I thought cvs will add them on commit. > 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. Yea, i can fix that. > 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 > > >
