pkgsrc-Changes archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]
CVS commit: pkgsrc/devel/cbmc
Module Name: pkgsrc
Committed By: alnsn
Date: Sat Oct 17 16:55:46 UTC 2026
Added Files:
pkgsrc/devel/cbmc: DESCR Makefile PLIST distinfo
pkgsrc/devel/cbmc/patches: patch-src_ansi-c_CMakeLists.txt
patch-src_ansi-c_library_stdio.c
Log Message:
Initial import of devel/cbmc version 6.10.0.
CBMC is a Bounded Model Checker for C and C++ programs. It supports
C89, C99, most of C11, C17, C23 and most compiler extensions provided
by gcc and Visual Studio. It also supports SystemC using Scoot. It
allows verifying 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.
To generate a diff of this commit:
cvs rdiff -u -r0 -r1.1 pkgsrc/devel/cbmc/DESCR pkgsrc/devel/cbmc/Makefile \
pkgsrc/devel/cbmc/PLIST pkgsrc/devel/cbmc/distinfo
cvs rdiff -u -r0 -r1.1 \
pkgsrc/devel/cbmc/patches/patch-src_ansi-c_CMakeLists.txt \
pkgsrc/devel/cbmc/patches/patch-src_ansi-c_library_stdio.c
Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.
Added files:
Index: pkgsrc/devel/cbmc/DESCR
diff -u /dev/null pkgsrc/devel/cbmc/DESCR:1.1
--- /dev/null Sat Oct 17 16:55:46 2026
+++ pkgsrc/devel/cbmc/DESCR Sat Oct 17 16:55:46 2026
@@ -0,0 +1,8 @@
+CBMC is a Bounded Model Checker for C and C++ programs. It supports
+C89, C99, most of C11, C17, C23 and most compiler extensions provided
+by gcc and Visual Studio. It also supports SystemC using Scoot. It
+allows verifying 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.
Index: pkgsrc/devel/cbmc/Makefile
diff -u /dev/null pkgsrc/devel/cbmc/Makefile:1.1
--- /dev/null Sat Oct 17 16:55:46 2026
+++ pkgsrc/devel/cbmc/Makefile Sat Oct 17 16:55:46 2026
@@ -0,0 +1,43 @@
+# $NetBSD: Makefile,v 1.1 2026/10/17 16:55:46 alnsn Exp $
+
+DISTNAME= cbmc-6.10.0
+GITHUB_TAG= cbmc-${PKGVERSION_NOREV}
+CATEGORIES= devel
+MASTER_SITES= ${MASTER_SITE_GITHUB:=diffblue/}
+DISTFILES= ${DEFAULT_DISTFILES} minisat2_2.2.1.orig.tar.gz
+SITES.minisat2_2.2.1.orig.tar.gz= ${MASTER_SITE_DEBIAN:=pool/main/m/minisat2/}
+EXTRACT_ONLY= ${DISTNAME}${EXTRACT_SUFX}
+
+MAINTAINER= pkgsrc-users%NetBSD.org@localhost
+HOMEPAGE= https://www.cprover.org/cbmc/
+COMMENT= Bounded Model Checker for C and C++ programs
+LICENSE= original-bsd
+
+USE_TOOLS+= flex bison bash gmake perl git
+USE_LANGUAGES= c c++
+USE_CXX_FEATURES+= c++17 filesystem
+
+CMAKE_CONFIGURE_ARGS+= -DWITH_JBMC=OFF
+
+EGDIR= ${PREFIX}/share/examples/cbmc
+CONF_FILES+= ${EGDIR}/bash_completion.d/cbmc \
+ ${PKG_SYSCONFDIR}/bash_completion.d/cbmc
+OWN_DIRS+= ${PKG_SYSCONFDIR}/bash_completion.d
+INSTALLATION_DIRS+= ${EGDIR}/bash_completion.d
+
+TEST_TARGET= test
+TEST_DEPENDS+= z3-[0-9]*:../../math/z3
+TEST_DEPENDS+= cvc5-[0-9]*:../../math/cvc5
+
+post-extract:
+ ${MKDIR} ${WRKSRC}/${CMAKE_BUILD_DIR}/minisat2-download/minisat2-download-prefix/src
+ ${CP} -p ${DISTDIR}/minisat2_2.2.1.orig.tar.gz \
+ ${WRKSRC}/${CMAKE_BUILD_DIR}/minisat2-download/minisat2-download-prefix/src/
+
+post-install:
+ ${MV} ${DESTDIR}${PREFIX}/etc/bash_completion.d/cbmc \
+ ${DESTDIR}${EGDIR}/bash_completion.d/cbmc
+ ${RMDIR} ${DESTDIR}${PREFIX}/etc/bash_completion.d
+
+.include "../../devel/cmake/build.mk"
+.include "../../mk/bsd.pkg.mk"
Index: pkgsrc/devel/cbmc/PLIST
diff -u /dev/null pkgsrc/devel/cbmc/PLIST:1.1
--- /dev/null Sat Oct 17 16:55:46 2026
+++ pkgsrc/devel/cbmc/PLIST Sat Oct 17 16:55:46 2026
@@ -0,0 +1,31 @@
+@comment $NetBSD: PLIST,v 1.1 2026/10/17 16:55:46 alnsn Exp $
+bin/cbmc
+bin/cprover
+bin/crangler
+bin/goto-analyzer
+bin/goto-cc
+bin/goto-diff
+bin/goto-gcc
+bin/goto-harness
+bin/goto-inspect
+bin/goto-instrument
+bin/goto-ld
+bin/goto-synthesizer
+bin/ls_parse.py
+bin/symtab2gb
+include/cprover/api.h
+include/cprover/api_options.h
+include/cprover/verification_result.h
+lib/libcprover.${PKGVERSION}.a
+man/man1/cbmc.1
+man/man1/crangler.1
+man/man1/goto-analyzer.1
+man/man1/goto-cc.1
+man/man1/goto-diff.1
+man/man1/goto-gcc.1
+man/man1/goto-harness.1
+man/man1/goto-instrument.1
+man/man1/goto-ld.1
+man/man1/goto-synthesizer.1
+man/man1/symtab2gb.1
+share/examples/cbmc/bash_completion.d/cbmc
Index: pkgsrc/devel/cbmc/distinfo
diff -u /dev/null pkgsrc/devel/cbmc/distinfo:1.1
--- /dev/null Sat Oct 17 16:55:46 2026
+++ pkgsrc/devel/cbmc/distinfo Sat Oct 17 16:55:46 2026
@@ -0,0 +1,10 @@
+$NetBSD: distinfo,v 1.1 2026/10/17 16:55:46 alnsn Exp $
+
+BLAKE2s (cbmc-6.10.0.tar.gz) = 35c20f0838e44704016ad1d9041b185e69b95d8ad7efcc1c7da096b056815f4d
+SHA512 (cbmc-6.10.0.tar.gz) = 87a8d0202c778c0699a11733f1d73f2239d9f91222644dc6fbffc820ece53f43621152191fa5443957c85608a0021e56b290959f10b518cb04133c40c7bf0dbe
+Size (cbmc-6.10.0.tar.gz) = 9162298 bytes
+BLAKE2s (minisat2_2.2.1.orig.tar.gz) = 94f71cea0f49ad903d690e23e4a4a3d9b2ddf19be462e3848716d6d67e4096f9
+SHA512 (minisat2_2.2.1.orig.tar.gz) = 279d8f65e5c848f6a1fded8890a907a91b9892ea3e33059a46373151ef64fe94de5e63b8a7512b74c3cd858f084bac818c36c6c5f6f503376f599a1335589949
+Size (minisat2_2.2.1.orig.tar.gz) = 44229 bytes
+SHA1 (patch-src_ansi-c_CMakeLists.txt) = 7886791c1a17a43e3ca21aa16f5ba4c741cd2c87
+SHA1 (patch-src_ansi-c_library_stdio.c) = ce9e9bf10f3c415066e1cfde9ded443d3dd01c36
Index: pkgsrc/devel/cbmc/patches/patch-src_ansi-c_CMakeLists.txt
diff -u /dev/null pkgsrc/devel/cbmc/patches/patch-src_ansi-c_CMakeLists.txt:1.1
--- /dev/null Sat Oct 17 16:55:46 2026
+++ pkgsrc/devel/cbmc/patches/patch-src_ansi-c_CMakeLists.txt Sat Oct 17 16:55:46 2026
@@ -0,0 +1,12 @@
+$NetBSD: patch-src_ansi-c_CMakeLists.txt,v 1.1 2026/10/17 16:55:46 alnsn Exp $
+
+Fix link errors, reported in https://github.com/diffblue/cbmc/issues/9088
+
+--- src/ansi-c/CMakeLists.txt.orig 2026-01-01 00:00:00.000000000 +0000
++++ src/ansi-c/CMakeLists.txt 2026-01-01 00:00:00.000000000 +0000
+@@ -144,3 +144,5 @@
+ generic_includes(ansi-c)
+
+ target_link_libraries(ansi-c analyses util linking goto-programs assembler)
++
++set_target_properties(ansi-c analyses PROPERTIES LINK_INTERFACE_MULTIPLICITY 3)
Index: pkgsrc/devel/cbmc/patches/patch-src_ansi-c_library_stdio.c
diff -u /dev/null pkgsrc/devel/cbmc/patches/patch-src_ansi-c_library_stdio.c:1.1
--- /dev/null Sat Oct 17 16:55:46 2026
+++ pkgsrc/devel/cbmc/patches/patch-src_ansi-c_library_stdio.c Sat Oct 17 16:55:46 2026
@@ -0,0 +1,27 @@
+$NetBSD: patch-src_ansi-c_library_stdio.c,v 1.1 2026/10/17 16:55:46 alnsn Exp $
+
+Undefine problematic macros.
+
+--- src/ansi-c/library/stdio.c.orig 2026-04-14 18:24:47.000000000 +0000
++++ src/ansi-c/library/stdio.c
+@@ -7,7 +7,7 @@
+ #endif
+
+ /* undefine macros in OpenBSD's stdio.h that are problematic to the checker. */
+-#if defined(__OpenBSD__)
++#if defined(__OpenBSD__) || defined(__FreeBSD__) || defined(__NetBSD__)
+ #undef getchar
+ #undef putchar
+ #undef getc
+@@ -373,7 +373,11 @@ __CPROVER_HIDE:;
+ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
+ int __VERIFIER_nondet_int(void);
+
++#if defined(__NetBSD__)
++char *__fgets_chk(char *str, int size, __CPROVER_size_t bufsize, FILE *stream)
++#else
+ char *__fgets_chk(char *str, __CPROVER_size_t bufsize, int size, FILE *stream)
++#endif
+ {
+ __CPROVER_HIDE:;
+ (void)bufsize;
Home |
Main Index |
Thread Index |
Old Index