SecBSD/ports
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

SecBSD's official ports repository

Browse source
This commit is contained in:
purplerain 2023-08-16 22:26:55 +00:00
commit 2c0afcbbf3
Signed by: purplerain
GPG key ID: F42C07F07E2E35B7
64331 changed files with 5339189 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

56
devel/cbmc/Makefile Normal file
View file

@ -0,0 +1,56 @@
COMMENT = Bounded Model Checker for C and C++ programs
GH_ACCOUNT = diffblue
GH_PROJECT = cbmc
GH_TAGNAME = cbmc-5.5
PKGNAME = ${GH_TAGNAME}
REVISION = 5
CATEGORIES = devel
HOMEPAGE = http://www.cprover.org/cbmc/
MAINTAINER = Mages Simon <mages.simon@googlemail.com>
# BSD
PERMIT_PACKAGE = Yes
WANTLIB += c m ${COMPILER_LIBCXX}
DISTFILES = ${GH_DISTFILE} \
minisat2_2.2.1.orig.tar.gz:0
MASTER_SITES0 = ${MASTER_SITE_DEBIAN:=main/m/minisat2/}
# C++11
COMPILER = base-clang ports-gcc
BUILD_DEPENDS = devel/bison
USE_GMAKE = Yes
MAKE_FLAGS = CC="${CC}" \
CXX="${CXX}" \
CFLAGS="-Wall ${CFLAGS}" \
CXXFLAGS="-Wall ${CXXFLAGS}" \
LINKFLAGS="${LDFLAGS}"
WRKSRC = ${WRKDIST}/src
post-extract:
mv ${WRKDIR}/minisat2-2.2.1 ${WRKDIST}/minisat-2.2.1
cd ${WRKDIST}/minisat-2.2.1; \
patch -z .bak -p1 < ../scripts/minisat-2.2.1-patch
do-install:
.for i in goto-analyzer goto-cc goto-diff goto-instrument cbmc
${INSTALL_PROGRAM} ${WRKBUILD}/${i}/${i} ${PREFIX}/bin/
.endfor
${INSTALL_MAN} ${WRKDIST}/doc/man/cbmc.1 ${PREFIX}/man/man1/
cd ${WRKDIST}/doc/ && find . -type d -exec ${INSTALL_DATA_DIR} \
${PREFIX}/share/doc/cbmc/{} \;
cd ${WRKDIST}/doc/ && find . -type f -exec ${INSTALL_DATA} \
${WRKDIST}/doc/{} ${PREFIX}/share/doc/cbmc/{} \;
rm ${PREFIX}/share/doc/cbmc/man/cbmc.1
rmdir ${PREFIX}/share/doc/cbmc/man/
.include <bsd.port.mk>

4
devel/cbmc/distinfo Normal file
View file

@ -0,0 +1,4 @@
SHA256 (cbmc-cbmc-5.5.tar.gz) = WpCpr4tTU4rAmDE32eN24uPDjYFYGieJAG8iNYsOnF4=
SHA256 (minisat2_2.2.1.orig.tar.gz) = 5Ur6PBksF1O8gHXAx+Em1cSV2QZuP5CiWICRFJrJykA=
SIZE (cbmc-cbmc-5.5.tar.gz) = 5274872
SIZE (minisat2_2.2.1.orig.tar.gz) = 44229

20
devel/cbmc/patches/patch-src_ansi-c_Makefile Normal file
View file

@ -0,0 +1,20 @@
Newer bison includes the defines file in the parser so the name must match.
Index: src/ansi-c/Makefile
--- src/ansi-c/Makefile.orig
+++ src/ansi-c/Makefile
@@ -36,12 +36,8 @@ all: ansi-c$(LIBEXT)
###############################################################################
-ansi_c_y.tab.cpp: parser.y
- $(YACC) $(YFLAGS) $$flags -pyyansi_c -d parser.y -o $@
-
-ansi_c_y.tab.h: ansi_c_y.tab.cpp
- if [ -e ansi_c_y.tab.hpp ] ; then mv ansi_c_y.tab.hpp ansi_c_y.tab.h ; else \
- mv ansi_c_y.tab.cpp.h ansi_c_y.tab.h ; fi
+ansi_c_y.tab.cpp ansi_c_y.tab.h: parser.y
+ $(YACC) $(YFLAGS) $$flags -pyyansi_c --defines=ansi_c_y.tab.h parser.y -o $@
ansi_c_lex.yy.cpp: scanner.l
$(LEX) -Pyyansi_c -o$@ scanner.l

11
devel/cbmc/patches/patch-src_big-int_allocainc_h Normal file
View file

@ -0,0 +1,11 @@
--- src/big-int/allocainc.h.orig Sun Oct 16 18:58:41 2016
+++ src/big-int/allocainc.h Sun Oct 16 18:58:58 2016
@@ -41,7 +41,7 @@ extern "C" void *alloca (unsigned);
# define alloca(X) __builtin_alloca(X)
-#elif defined __FreeBSD__ || defined __FreeBSD_kernel__
+#elif defined __FreeBSD__ || defined __FreeBSD_kernel__ || defined __OpenBSD__
# include <stdlib.h>

32
devel/cbmc/patches/patch-src_common Normal file
View file

@ -0,0 +1,32 @@
--- src/common.orig Sat Aug 20 14:08:13 2016
+++ src/common Fri Oct 14 16:29:34 2016
@@ -9,6 +9,8 @@ else ifeq ($(uname),Darwin)
BUILD_ENV_ := OSX
else ifeq ($(uname),FreeBSD)
BUILD_ENV_ := FreeBSD
+else ifeq ($(uname),OpenBSD)
+ BUILD_ENV_ := OpenBSD
else ifeq ($(filter-out MINGW32_%, $(uname)),)
BUILD_ENV_ := MinGW
else ifeq ($(filter-out CYGWIN_%, $(uname)),)
@@ -20,7 +22,7 @@ else
BUILD_ENV_ := $(BUILD_ENV)
endif
-ifeq ($(filter-out Unix MinGW OSX OSX_Universal FreeBSD,$(BUILD_ENV_)),)
+ifeq ($(filter-out Unix MinGW OSX OSX_Universal FreeBSD OpenBSD,$(BUILD_ENV_)),)
# Linux-ish
LIBEXT = .a
OBJEXT = .o
@@ -59,6 +61,11 @@ ifeq ($(filter-out OSX OSX_Universal,$(BUILD_ENV_)),)
else ifeq ($(filter-out FreeBSD,$(BUILD_ENV_)),)
CP_CXXFLAGS +=
LINKLIB = ar rcT $@ $^
+ LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS)
+ LINKNATIVE = $(HOSTCXX) -o $@ $^
+else ifeq ($(filter-out OpenBSD,$(BUILD_ENV_)),)
+ CP_CXXFLAGS +=
+ LINKLIB = ar rc $@ $^
LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS)
LINKNATIVE = $(HOSTCXX) -o $@ $^
ifeq ($(origin CC),default)

20
devel/cbmc/patches/patch-src_jsil_Makefile Normal file
View file

@ -0,0 +1,20 @@
Newer bison includes the defines file in the parser so the name must match.
Index: src/jsil/Makefile
--- src/jsil/Makefile.orig
+++ src/jsil/Makefile
@@ -19,12 +19,8 @@ all: jsil$(LIBEXT)
jsil$(LIBEXT): $(OBJ)
$(LINKLIB)
-jsil_y.tab.cpp: parser.y
- $(YACC) $(YFLAGS) $$flags -pyyjsil -d parser.y -o $@
-
-jsil_y.tab.h: jsil_y.tab.cpp
- if [ -e jsil_y.tab.hpp ] ; then mv jsil_y.tab.hpp jsil_y.tab.h ; else \
- mv jsil_y.tab.cpp.h jsil_y.tab.h ; fi
+jsil_y.tab.cpp jsil_y.tab.h: parser.y
+ $(YACC) $(YFLAGS) $$flags -pyyjsil --defines=jsil_y.tab.h parser.y -o $@
jsil_lex.yy.cpp: scanner.l
$(LEX) -Pyyjsil -o$@ scanner.l

20
devel/cbmc/patches/patch-src_json_Makefile Normal file
View file

@ -0,0 +1,20 @@
Newer bison includes the defines file in the parser so the name must match.
Index: src/json/Makefile
--- src/json/Makefile.orig
+++ src/json/Makefile
@@ -15,12 +15,8 @@ all: json$(LIBEXT)
json$(LIBEXT): $(OBJ)
$(LINKLIB)
-json_y.tab.cpp: parser.y
- $(YACC) $(YFLAGS) $$flags -pyyjson -d parser.y -o $@
-
-json_y.tab.h: json_y.tab.cpp
- if [ -e json_y.tab.hpp ] ; then mv json_y.tab.hpp $@ ; else \
- mv json_y.tab.cpp.h $@ ; fi
+json_y.tab.cpp json_y.tab.h: parser.y
+ $(YACC) $(YFLAGS) $$flags -pyyjson --defines=json_y.tab.h parser.y -o $@
json_lex.yy.cpp: scanner.l
$(LEX) -Pyyjson -o$@ scanner.l

20
devel/cbmc/patches/patch-src_memory-models_Makefile Normal file
View file

@ -0,0 +1,20 @@
Newer bison includes the defines file in the parser so the name must match.
Index: src/memory-models/Makefile
--- src/memory-models/Makefile.orig
+++ src/memory-models/Makefile
@@ -16,12 +16,8 @@ all: mmcc$(EXEEXT)
###############################################################################
-mm_y.tab.cpp: parser.y
- $(YACC) $(YFLAGS) $$flags -pyymm -d parser.y -o $@
-
-mm_y.tab.h: mm_y.tab.cpp
- if [ -e mm_y.tab.hpp ] ; then mv mm_y.tab.hpp mm_y.tab.h ; else \
- mv mm_y.tab.cpp.h mm_y.tab.h ; fi
+mm_y.tab.cpp mm_y.tab.h: parser.y
+ $(YACC) $(YFLAGS) $$flags -pyymm --defines=mm_y.tab.h parser.y -o $@
mm_lex.yy.cpp: scanner.l
$(LEX) -Pyymm -o$@ scanner.l

20
devel/cbmc/patches/patch-src_xmllang_Makefile Normal file
View file

@ -0,0 +1,20 @@
Newer bison includes the defines file in the parser so the name must match.
Index: src/xmllang/Makefile
--- src/xmllang/Makefile.orig
+++ src/xmllang/Makefile
@@ -15,12 +15,8 @@ all: xmllang$(LIBEXT)
xmllang$(LIBEXT): $(OBJ)
$(LINKLIB)
-xml_y.tab.cpp: parser.y
- $(YACC) $(YFLAGS) $$flags -pyyxml -d parser.y -o $@
-
-xml_y.tab.h: xml_y.tab.cpp
- if [ -e xml_y.tab.hpp ] ; then mv xml_y.tab.hpp $@ ; else \
- mv xml_y.tab.cpp.h $@ ; fi
+xml_y.tab.cpp xml_y.tab.h: parser.y
+ $(YACC) $(YFLAGS) $$flags -pyyxml --defines=xml_y.tab.h parser.y -o $@
xml_lex.yy.cpp: scanner.l
$(LEX) -Pyyxml -o$@ scanner.l

19
devel/cbmc/pkg/DESCR Normal file
View file

@ -0,0 +1,19 @@
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, and has experimental support for Java
Bytecode.
CBMC verifies array bounds (buffer overflows), pointer safety, exceptions
and user-specified assertions. 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 resulting
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. Recommended solvers 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.

171
devel/cbmc/pkg/PLIST Normal file
View file

@ -0,0 +1,171 @@
@bin bin/cbmc
@bin bin/goto-analyzer
@bin bin/goto-cc
@bin bin/goto-diff
@bin bin/goto-instrument
@man man/man1/cbmc.1
share/doc/cbmc/
share/doc/cbmc/guide/
share/doc/cbmc/guide/CBMC-guide.tex
share/doc/cbmc/html-manual/
share/doc/cbmc/html-manual/api.shtml
share/doc/cbmc/html-manual/architecture.shtml
share/doc/cbmc/html-manual/binsearch.c
share/doc/cbmc/html-manual/boop-example/
share/doc/cbmc/html-manual/boop-example/driver.c
share/doc/cbmc/html-manual/boop-example/driver.h
share/doc/cbmc/html-manual/boop-example/kdev_t.h
share/doc/cbmc/html-manual/boop-example/modules.h
share/doc/cbmc/html-manual/boop-example/spec.c
share/doc/cbmc/html-manual/c_to_ir.svg
share/doc/cbmc/html-manual/cbmc-loops.shtml
share/doc/cbmc/html-manual/cbmc.shtml
share/doc/cbmc/html-manual/cegar-1.png
share/doc/cbmc/html-manual/counter.c
share/doc/cbmc/html-manual/counter.v
share/doc/cbmc/html-manual/cprover-source.shtml
share/doc/cbmc/html-manual/expr.c
share/doc/cbmc/html-manual/expr.svg
share/doc/cbmc/html-manual/file1.c
share/doc/cbmc/html-manual/file2.c
share/doc/cbmc/html-manual/footer.inc
share/doc/cbmc/html-manual/gcc-wrap.c
share/doc/cbmc/html-manual/goto-cc-apache.shtml
share/doc/cbmc/html-manual/goto-cc-linux.shtml
share/doc/cbmc/html-manual/goto-cc-rockbox.shtml
share/doc/cbmc/html-manual/goto-cc-variants.shtml
share/doc/cbmc/html-manual/goto-cc-visual-studio.shtml
share/doc/cbmc/html-manual/goto-cc.shtml
share/doc/cbmc/html-manual/goto_program.svg
share/doc/cbmc/html-manual/header.inc
share/doc/cbmc/html-manual/highlight/
share/doc/cbmc/html-manual/highlight/CHANGES.md
share/doc/cbmc/html-manual/highlight/LICENSE
share/doc/cbmc/html-manual/highlight/README.md
share/doc/cbmc/html-manual/highlight/README.ru.md
share/doc/cbmc/html-manual/highlight/highlight.pack.js
share/doc/cbmc/html-manual/highlight/styles/
share/doc/cbmc/html-manual/highlight/styles/agate.css
share/doc/cbmc/html-manual/highlight/styles/androidstudio.css
share/doc/cbmc/html-manual/highlight/styles/arduino-light.css
share/doc/cbmc/html-manual/highlight/styles/arta.css
share/doc/cbmc/html-manual/highlight/styles/ascetic.css
share/doc/cbmc/html-manual/highlight/styles/atelier-cave-dark.css
share/doc/cbmc/html-manual/highlight/styles/atelier-cave-light.css
share/doc/cbmc/html-manual/highlight/styles/atelier-dune-dark.css
share/doc/cbmc/html-manual/highlight/styles/atelier-dune-light.css
share/doc/cbmc/html-manual/highlight/styles/atelier-estuary-dark.css
share/doc/cbmc/html-manual/highlight/styles/atelier-estuary-light.css
share/doc/cbmc/html-manual/highlight/styles/atelier-forest-dark.css
share/doc/cbmc/html-manual/highlight/styles/atelier-forest-light.css
share/doc/cbmc/html-manual/highlight/styles/atelier-heath-dark.css
share/doc/cbmc/html-manual/highlight/styles/atelier-heath-light.css
share/doc/cbmc/html-manual/highlight/styles/atelier-lakeside-dark.css
share/doc/cbmc/html-manual/highlight/styles/atelier-lakeside-light.css
share/doc/cbmc/html-manual/highlight/styles/atelier-plateau-dark.css
share/doc/cbmc/html-manual/highlight/styles/atelier-plateau-light.css
share/doc/cbmc/html-manual/highlight/styles/atelier-savanna-dark.css
share/doc/cbmc/html-manual/highlight/styles/atelier-savanna-light.css
share/doc/cbmc/html-manual/highlight/styles/atelier-seaside-dark.css
share/doc/cbmc/html-manual/highlight/styles/atelier-seaside-light.css
share/doc/cbmc/html-manual/highlight/styles/atelier-sulphurpool-dark.css
share/doc/cbmc/html-manual/highlight/styles/atelier-sulphurpool-light.css
share/doc/cbmc/html-manual/highlight/styles/brown-paper.css
share/doc/cbmc/html-manual/highlight/styles/brown-papersq.png
share/doc/cbmc/html-manual/highlight/styles/codepen-embed.css
share/doc/cbmc/html-manual/highlight/styles/color-brewer.css
share/doc/cbmc/html-manual/highlight/styles/dark.css
share/doc/cbmc/html-manual/highlight/styles/darkula.css
share/doc/cbmc/html-manual/highlight/styles/default.css
share/doc/cbmc/html-manual/highlight/styles/docco.css
share/doc/cbmc/html-manual/highlight/styles/dracula.css
share/doc/cbmc/html-manual/highlight/styles/far.css
share/doc/cbmc/html-manual/highlight/styles/foundation.css
share/doc/cbmc/html-manual/highlight/styles/github-gist.css
share/doc/cbmc/html-manual/highlight/styles/github.css
share/doc/cbmc/html-manual/highlight/styles/googlecode.css
share/doc/cbmc/html-manual/highlight/styles/grayscale.css
share/doc/cbmc/html-manual/highlight/styles/gruvbox-dark.css
share/doc/cbmc/html-manual/highlight/styles/gruvbox-light.css
share/doc/cbmc/html-manual/highlight/styles/hopscotch.css
share/doc/cbmc/html-manual/highlight/styles/hybrid.css
share/doc/cbmc/html-manual/highlight/styles/idea.css
share/doc/cbmc/html-manual/highlight/styles/ir-black.css
share/doc/cbmc/html-manual/highlight/styles/kimbie.dark.css
share/doc/cbmc/html-manual/highlight/styles/kimbie.light.css
share/doc/cbmc/html-manual/highlight/styles/magula.css
share/doc/cbmc/html-manual/highlight/styles/mono-blue.css
share/doc/cbmc/html-manual/highlight/styles/monokai-sublime.css
share/doc/cbmc/html-manual/highlight/styles/monokai.css
share/doc/cbmc/html-manual/highlight/styles/obsidian.css
share/doc/cbmc/html-manual/highlight/styles/paraiso-dark.css
share/doc/cbmc/html-manual/highlight/styles/paraiso-light.css
share/doc/cbmc/html-manual/highlight/styles/pojoaque.css
share/doc/cbmc/html-manual/highlight/styles/pojoaque.jpg
share/doc/cbmc/html-manual/highlight/styles/purebasic.css
share/doc/cbmc/html-manual/highlight/styles/qtcreator_dark.css
share/doc/cbmc/html-manual/highlight/styles/qtcreator_light.css
share/doc/cbmc/html-manual/highlight/styles/railscasts.css
share/doc/cbmc/html-manual/highlight/styles/rainbow.css
share/doc/cbmc/html-manual/highlight/styles/school-book.css
share/doc/cbmc/html-manual/highlight/styles/school-book.png
share/doc/cbmc/html-manual/highlight/styles/solarized-dark.css
share/doc/cbmc/html-manual/highlight/styles/solarized-light.css
share/doc/cbmc/html-manual/highlight/styles/sunburst.css
share/doc/cbmc/html-manual/highlight/styles/tomorrow-night-blue.css
share/doc/cbmc/html-manual/highlight/styles/tomorrow-night-bright.css
share/doc/cbmc/html-manual/highlight/styles/tomorrow-night-eighties.css
share/doc/cbmc/html-manual/highlight/styles/tomorrow-night.css
share/doc/cbmc/html-manual/highlight/styles/tomorrow.css
share/doc/cbmc/html-manual/highlight/styles/vs.css
share/doc/cbmc/html-manual/highlight/styles/xcode.css
share/doc/cbmc/html-manual/highlight/styles/xt256.css
share/doc/cbmc/html-manual/highlight/styles/zenburn.css
share/doc/cbmc/html-manual/hwsw-inputs.shtml
share/doc/cbmc/html-manual/hwsw-mapping.shtml
share/doc/cbmc/html-manual/hwsw-tutorial.shtml
share/doc/cbmc/html-manual/hwsw.shtml
share/doc/cbmc/html-manual/index.shtml
share/doc/cbmc/html-manual/installation-cbmc.shtml
share/doc/cbmc/html-manual/installation-plugin.shtml
share/doc/cbmc/html-manual/installation-satabs.shtml
share/doc/cbmc/html-manual/introduction.shtml
share/doc/cbmc/html-manual/ireptree.svg
share/doc/cbmc/html-manual/libraries.shtml
share/doc/cbmc/html-manual/lock-example-fixed.c
share/doc/cbmc/html-manual/lock-example.c
share/doc/cbmc/html-manual/modeling-assertions.shtml
share/doc/cbmc/html-manual/modeling-floating-point.shtml
share/doc/cbmc/html-manual/modeling-nondet.shtml
share/doc/cbmc/html-manual/modeling-pointers.shtml
share/doc/cbmc/html-manual/properties.shtml
share/doc/cbmc/html-manual/refinement.png
share/doc/cbmc/html-manual/ring_buffer1.c
share/doc/cbmc/html-manual/ring_buffer2.c
share/doc/cbmc/html-manual/satabs-aeon.shtml
share/doc/cbmc/html-manual/satabs-background.shtml
share/doc/cbmc/html-manual/satabs-driver.shtml
share/doc/cbmc/html-manual/satabs-tutorials.shtml
share/doc/cbmc/html-manual/satabs.shtml
share/doc/cbmc/html-manual/states.png
share/doc/cbmc/slides/
share/doc/cbmc/slides/cbmc-latex-beamer/
share/doc/cbmc/slides/cbmc-latex-beamer/arrow.pdf
share/doc/cbmc/slides/cbmc-latex-beamer/bmc-loop.mp
share/doc/cbmc/slides/cbmc-latex-beamer/cbmc-flow.fig
share/doc/cbmc/slides/cbmc-latex-beamer/cbmc-logo-medium.png
share/doc/cbmc/slides/cbmc-latex-beamer/cbmc-slides.tex
share/doc/cbmc/slides/cbmc-latex-beamer/do_figures
share/doc/cbmc/slides/cbmc-latex-beamer/frontend.fig
share/doc/cbmc/slides/cbmc-latex-beamer/gradient_box_green.pdf
share/doc/cbmc/slides/cbmc-latex-beamer/gradient_box_red.pdf
share/doc/cbmc/slides/cbmc-latex-beamer/gradient_box_yellow.pdf
share/doc/cbmc/slides/cbmc-latex-beamer/header.tex
share/doc/cbmc/slides/cbmc-latex-beamer/sa-sat-progress.pdf
share/doc/cbmc/slides/cbmc-latex-beamer/sha-example.mp
share/doc/cbmc/slides/cbmc-latex-beamer/unrolling-cfg.mp
share/doc/cbmc/slides/cbmc-latex-beamer/unrolling-full.mp
share/doc/cbmc/slides/cbmc-latex-beamer/unrolling.mp
share/doc/cbmc/slides/cprover-overview-latex-beamer/
share/doc/cbmc/slides/cprover-overview-latex-beamer/cprover-overview-slides.tex
share/doc/cbmc/slides/cprover-overview-latex-beamer/header.tex