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
Ok, will fix that.
> 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
Yea, i can fix that.
> ## 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
> (/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
> > 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,
> > most of C11 and most compiler extensions provided by gcc and Visual
> Studio. It
> > also supports SystemC using Scoot. We have recently added experimental
> > for Java Bytecode.
> > CBMC verifies array bounds (buffer overflows), pointer safety,
> > and user-specified as??ser??tions. Furthermore, it can check C and C++
> > consistency with other languages, such as Verilog. The verification is
> > performed by unwinding the loops in the program and passing the
> > equation to a decision procedure.
> > While CBMC is aimed for embedded software, it also supports dynamic
> > allocation using malloc and new.
> > CBMC comes with a built-in solver for bit-vector formulas that is based
> > MiniSat. As an alternative, CBMC has featured support for external SMT
> > 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