git: 85f08f2fd423 - main - devel/cbmc: witch to the recommended cmake build and add test support
- Go to: [ bottom of page ] [ top of archives ] [ this month ]
Date: Sat, 20 Jun 2026 20:53:42 UTC
The branch main has been updated by olivier:
URL: https://cgit.FreeBSD.org/ports/commit/?id=85f08f2fd423ae8d42e5deeed6a3321e6741c0c4
commit 85f08f2fd423ae8d42e5deeed6a3321e6741c0c4
Author: Olivier Cochard <olivier@FreeBSD.org>
AuthorDate: 2026-06-20 20:43:44 +0000
Commit: Olivier Cochard <olivier@FreeBSD.org>
CommitDate: 2026-06-20 20:51:52 +0000
devel/cbmc: witch to the recommended cmake build and add test support
PR: 296170
Reported by: siva
---
devel/cbmc/Makefile | 45 +++++++----------
.../patch-minisat-2.2.1_minisat_core_Solver.cc | 20 --------
.../patch-minisat-2.2.1_minisat_core_SolverTypes.h | 59 ----------------------
.../patch-minisat-2.2.1_minisat_mtl_IntTypes.h | 12 -----
.../files/patch-minisat-2.2.1_minisat_mtl_Vec.h | 16 ------
.../files/patch-minisat-2.2.1_minisat_mtl_XAlloc.h | 19 -------
.../patch-minisat-2.2.1_minisat_simp_SimpSolver.cc | 37 --------------
.../patch-minisat-2.2.1_minisat_utils_Options.cc | 15 ------
.../patch-minisat-2.2.1_minisat_utils_Options.h | 30 -----------
.../patch-minisat-2.2.1_minisat_utils_ParseUtils.h | 33 ------------
.../patch-minisat-2.2.1_minisat_utils_System.h | 11 ----
devel/cbmc/files/patch-src_ansi-c_library_stdio.c | 13 +++++
devel/cbmc/pkg-plist | 19 ++++---
13 files changed, 45 insertions(+), 284 deletions(-)
diff --git a/devel/cbmc/Makefile b/devel/cbmc/Makefile
index 0743231deea4..dd76cebffe07 100644
--- a/devel/cbmc/Makefile
+++ b/devel/cbmc/Makefile
@@ -1,6 +1,7 @@
PORTNAME= cbmc
-PORTVERSION= 6.9.0
DISTVERSIONPREFIX= cbmc-
+DISTVERSION= 6.9.0
+PORTREVISION= 1
CATEGORIES= devel
MASTER_SITES= DEBIAN/pool/main/m/minisat2:minisat
DISTFILES= minisat2_2.2.1.orig.tar.gz:minisat
@@ -12,35 +13,27 @@ WWW= https://github.com/diffblue/cbmc
LICENSE= BSD4CLAUSE
LICENSE_FILE= ${WRKSRC}/LICENSE
-BUILD_DEPENDS= ${LOCALBASE}/bin/flex:textproc/flex
-RUN_DEPENDS= ${LOCALBASE}/bin/cvc5:math/cvc5 \
- ${LOCALBASE}/bin/z3:math/z3
+BUILD_DEPENDS= flex:textproc/flex \
+ bash:shells/bash \
+ git:devel/git@lite \
+ jq:textproc/jq
+RUN_DEPENDS= cvc5:math/cvc5 \
+ z3:math/z3
-USES= gmake bison python shebangfix
+USES= cmake bison python shebangfix perl5
+USE_PERL5= build
USE_GITHUB= yes
GH_ACCOUNT= diffblue
SHEBANG_FILES= ${WRKSRC}/scripts/ls_parse.py
-WRKSRC_minisat= ${WRKDIR}/minisat2-2.2.1
-
-post-patch:
- @${REINPLACE_CMD} -e 's|.*git describe --tags.*|GIT_INFO = ${PORTNAME}-${PORTVERSION}|' \
- ${WRKSRC}/src/util/Makefile
-post-extract:
- @${MV} ${WRKSRC_minisat} ${WRKSRC}/minisat-2.2.1
-
-do-build:
- @${MKDIR} ${STAGEDIR}
- cd ${WRKSRC} && ${GMAKE} -C src -j${MAKE_JOBS_NUMBER}
-
-do-install:
-. for x in cbmc crangler goto-analyzer goto-cc goto-diff goto-instrument \
- goto-inspect goto-harness goto-synthesizer symtab2gb
- ${INSTALL_PROGRAM} ${WRKSRC}/src/${x}/${x} ${STAGEDIR}${PREFIX}/bin/
- ${INSTALL_MAN} ${WRKSRC}/doc/man/${x}.1 ${STAGEDIR}${PREFIX}/share/man/man1/
-. endfor
- ${LN} -sf goto-cc ${STAGEDIR}${PREFIX}/bin/goto-gcc
- ${LN} -sf goto-cc ${STAGEDIR}${PREFIX}/bin/goto-ld
- ${INSTALL_SCRIPT} ${WRKSRC}/scripts/ls_parse.py ${STAGEDIR}${PREFIX}/bin/
+
+CMAKE_OFF= WITH_JBMC
+
+pre-extract:
+ ${MKDIR} ${BUILD_WRKSRC}/minisat2-download/minisat2-download-prefix/src
+ ${CP} ${DISTDIR}/minisat2_2.2.1.orig.tar.gz ${BUILD_WRKSRC}/minisat2-download/minisat2-download-prefix/src/
+
+do-test:
+ cd ${BUILD_WRKSRC} && ctest . -V -L CORE
.include <bsd.port.mk>
diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_Solver.cc b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_Solver.cc
deleted file mode 100644
index c15c2f12fb0a..000000000000
--- a/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_Solver.cc
+++ /dev/null
@@ -1,20 +0,0 @@
---- minisat-2.2.1/minisat/core/Solver.cc.orig 2011-02-21 13:31:17 UTC
-+++ minisat-2.2.1/minisat/core/Solver.cc
-@@ -210,7 +210,7 @@ void Solver::cancelUntil(int level) {
- for (int c = trail.size()-1; c >= trail_lim[level]; c--){
- Var x = var(trail[c]);
- assigns [x] = l_Undef;
-- if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
-+ if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last()))
- polarity[x] = sign(trail[c]);
- insertVarOrder(x); }
- qhead = trail_lim[level];
-@@ -666,7 +666,7 @@ lbool Solver::search(int nof_conflicts)
-
- }else{
- // NO CONFLICT
-- if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){
-+ if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || !withinBudget()){
- // Reached bound on number of conflicts:
- progress_estimate = progressEstimate();
- cancelUntil(0);
diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_SolverTypes.h b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_SolverTypes.h
deleted file mode 100644
index fa26c6372b36..000000000000
--- a/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_SolverTypes.h
+++ /dev/null
@@ -1,59 +0,0 @@
---- minisat-2.2.1/minisat/core/SolverTypes.h.orig 2011-02-21 13:31:17 UTC
-+++ minisat-2.2.1/minisat/core/SolverTypes.h
-@@ -47,7 +47,7 @@ struct Lit {
- int x;
-
- // Use this as a constructor:
-- friend Lit mkLit(Var var, bool sign = false);
-+ //friend Lit mkLit(Var var, bool sign = false);
-
- bool operator == (Lit p) const { return x == p.x; }
- bool operator != (Lit p) const { return x != p.x; }
-@@ -55,7 +55,7 @@ struct Lit {
- };
-
-
--inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
-+inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; }
- inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; }
- inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
- inline bool sign (Lit p) { return p.x & 1; }
-@@ -127,7 +127,10 @@ class Clause {
- unsigned has_extra : 1;
- unsigned reloced : 1;
- unsigned size : 27; } header;
-+#include <util/pragma_push.def>
-+#include <util/pragma_wzero_length_array.def>
- union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];
-+#include <util/pragma_pop.def>
-
- friend class ClauseAllocator;
-
-@@ -142,11 +145,12 @@ class Clause {
- for (int i = 0; i < ps.size(); i++)
- data[i].lit = ps[i];
-
-- if (header.has_extra)
-+ if (header.has_extra) {
- if (header.learnt)
- data[header.size].act = 0;
- else
- calcAbstraction();
-+ }
- }
-
- // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
-@@ -157,11 +161,12 @@ class Clause {
- for (int i = 0; i < from.size(); i++)
- data[i].lit = from[i];
-
-- if (header.has_extra)
-+ if (header.has_extra) {
- if (header.learnt)
- data[header.size].act = from.data[header.size].act;
- else
- data[header.size].abs = from.data[header.size].abs;
-+ }
- }
-
- public:
diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h
deleted file mode 100644
index d8c9ddedb701..000000000000
--- a/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h
+++ /dev/null
@@ -1,12 +0,0 @@
---- minisat-2.2.1/minisat/mtl/IntTypes.h.orig 2011-02-21 13:31:17 UTC
-+++ minisat-2.2.1/minisat/mtl/IntTypes.h
-@@ -31,7 +31,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OT
- #else
-
- # include <stdint.h>
-+#ifndef _MSC_VER
- # include <inttypes.h>
-+#endif
-
- #endif
-
diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_Vec.h b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_Vec.h
deleted file mode 100644
index b3062972c5c9..000000000000
--- a/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_Vec.h
+++ /dev/null
@@ -1,16 +0,0 @@
---- minisat-2.2.1/minisat/mtl/Vec.h.orig 2011-02-21 13:31:17 UTC
-+++ minisat-2.2.1/minisat/mtl/Vec.h
-@@ -96,9 +96,11 @@ void vec<T>::capacity(int min_cap) {
- void vec<T>::capacity(int min_cap) {
- if (cap >= min_cap) return;
- int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
-- if (add > INT_MAX - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)
-+ if (add > INT_MAX - cap)
- throw OutOfMemoryException();
-- }
-+
-+ data = (T*)xrealloc(data, (cap += add) * sizeof(T));
-+}
-
-
- template<class T>
diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_XAlloc.h b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_XAlloc.h
deleted file mode 100644
index 8c8b9680bf6d..000000000000
--- a/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_XAlloc.h
+++ /dev/null
@@ -1,19 +0,0 @@
---- minisat-2.2.1/minisat/mtl/XAlloc.h.orig 2011-02-21 13:31:17 UTC
-+++ minisat-2.2.1/minisat/mtl/XAlloc.h
-@@ -21,7 +21,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OT
- #ifndef Minisat_XAlloc_h
- #define Minisat_XAlloc_h
-
--#include <errno.h>
- #include <stdlib.h>
-
- namespace Minisat {
-@@ -33,7 +32,7 @@ static inline void* xrealloc(void *ptr, size_t size)
- static inline void* xrealloc(void *ptr, size_t size)
- {
- void* mem = realloc(ptr, size);
-- if (mem == NULL && errno == ENOMEM){
-+ if (mem == NULL){
- throw OutOfMemoryException();
- }else
- return mem;
diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_simp_SimpSolver.cc b/devel/cbmc/files/patch-minisat-2.2.1_minisat_simp_SimpSolver.cc
deleted file mode 100644
index c83101829f03..000000000000
--- a/devel/cbmc/files/patch-minisat-2.2.1_minisat_simp_SimpSolver.cc
+++ /dev/null
@@ -1,37 +0,0 @@
---- minisat-2.2.1/minisat/simp/SimpSolver.cc.orig 2011-02-21 13:31:17 UTC
-+++ minisat-2.2.1/minisat/simp/SimpSolver.cc
-@@ -130,8 +130,6 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_s
- return result;
- }
-
--
--
- bool SimpSolver::addClause_(vec<Lit>& ps)
- {
- #ifndef NDEBUG
-@@ -227,10 +225,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause
- if (var(qs[i]) != v){
- for (int j = 0; j < ps.size(); j++)
- if (var(ps[j]) == var(qs[i]))
-+ {
- if (ps[j] == ~qs[i])
- return false;
- else
- goto next;
-+ }
- out_clause.push(qs[i]);
- }
- next:;
-@@ -261,10 +261,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause
- if (var(__qs[i]) != v){
- for (int j = 0; j < ps.size(); j++)
- if (var(__ps[j]) == var(__qs[i]))
-+ {
- if (__ps[j] == ~__qs[i])
- return false;
- else
- goto next;
-+ }
- size++;
- }
- next:;
diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_Options.cc b/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_Options.cc
deleted file mode 100644
index 84b5f289e8a5..000000000000
--- a/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_Options.cc
+++ /dev/null
@@ -1,15 +0,0 @@
---- minisat-2.2.1/minisat/utils/Options.cc.orig 2011-02-21 13:31:17 UTC
-+++ minisat-2.2.1/minisat/utils/Options.cc
-@@ -43,10 +43,12 @@ void Minisat::parseOptions(int& argc, char** argv, boo
- }
-
- if (!parsed_ok)
-+ {
- if (strict && match(argv[i], "-"))
- fprintf(stderr, "ERROR! Unknown flag \"%s\". Use '--%shelp' for help.\n", argv[i], Option::getHelpPrefixString()), exit(1);
- else
- argv[j++] = argv[i];
-+ }
- }
- }
-
diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_Options.h b/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_Options.h
deleted file mode 100644
index c844c16940d9..000000000000
--- a/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_Options.h
+++ /dev/null
@@ -1,30 +0,0 @@
---- minisat-2.2.1/minisat/utils/Options.h.orig 2011-02-21 13:31:17 UTC
-+++ minisat-2.2.1/minisat/utils/Options.h
-@@ -60,7 +60,7 @@ class Option
- struct OptionLt {
- bool operator()(const Option* x, const Option* y) {
- int test1 = strcmp(x->category, y->category);
-- return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0;
-+ return test1 < 0 || (test1 == 0 && strcmp(x->type_name, y->type_name) < 0);
- }
- };
-
-@@ -282,15 +282,15 @@ class Int64Option : public Option
- if (range.begin == INT64_MIN)
- fprintf(stderr, "imin");
- else
-- fprintf(stderr, "%4"PRIi64, range.begin);
-+ fprintf(stderr, "%4" PRIi64, range.begin);
-
- fprintf(stderr, " .. ");
- if (range.end == INT64_MAX)
- fprintf(stderr, "imax");
- else
-- fprintf(stderr, "%4"PRIi64, range.end);
-+ fprintf(stderr, "%4" PRIi64, range.end);
-
-- fprintf(stderr, "] (default: %"PRIi64")\n", value);
-+ fprintf(stderr, "] (default: %" PRIi64 ")\n", value);
- if (verbose){
- fprintf(stderr, "\n %s\n", description);
- fprintf(stderr, "\n");
diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_ParseUtils.h b/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_ParseUtils.h
deleted file mode 100644
index a0b231103805..000000000000
--- a/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_ParseUtils.h
+++ /dev/null
@@ -1,33 +0,0 @@
---- minisat-2.2.1/minisat/utils/ParseUtils.h.orig 2011-02-21 13:31:17 UTC
-+++ minisat-2.2.1/minisat/utils/ParseUtils.h
-@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OT
- #include <stdlib.h>
- #include <stdio.h>
-
--#include <zlib.h>
-+//#include <zlib.h>
-
- namespace Minisat {
-
-@@ -35,7 +35,7 @@ class StreamBuffer {
-
-
- class StreamBuffer {
-- gzFile in;
-+ //gzFile in;
- unsigned char buf[buffer_size];
- int pos;
- int size;
-@@ -43,10 +43,10 @@ class StreamBuffer {
- void assureLookahead() {
- if (pos >= size) {
- pos = 0;
-- size = gzread(in, buf, sizeof(buf)); } }
-+ /*size = gzread(in, buf, sizeof(buf));*/ } }
-
- public:
-- explicit StreamBuffer(gzFile i) : in(i), pos(0), size(0) { assureLookahead(); }
-+ //explicit StreamBuffer(gzFile i) : in(i), pos(0), size(0) { assureLookahead(); }
-
- int operator * () const { return (pos >= size) ? EOF : buf[pos]; }
- void operator ++ () { pos++; assureLookahead(); }
diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_System.h b/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_System.h
deleted file mode 100644
index a49382def0dc..000000000000
--- a/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_System.h
+++ /dev/null
@@ -1,11 +0,0 @@
---- minisat-2.2.1/minisat/utils/System.h.orig 2011-02-21 13:31:17 UTC
-+++ minisat-2.2.1/minisat/utils/System.h
-@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OT
- #ifndef Minisat_System_h
- #define Minisat_System_h
-
--#if defined(__linux__)
-+#if defined(__linux__) && defined(__GLIBC__)
- #include <fpu_control.h>
- #endif
-
diff --git a/devel/cbmc/files/patch-src_ansi-c_library_stdio.c b/devel/cbmc/files/patch-src_ansi-c_library_stdio.c
new file mode 100644
index 000000000000..343017db4eaa
--- /dev/null
+++ b/devel/cbmc/files/patch-src_ansi-c_library_stdio.c
@@ -0,0 +1,13 @@
+--- src/ansi-c/library/stdio.c.orig 2026-06-20 15:25:39 UTC
++++ src/ansi-c/library/stdio.c
+@@ -6,8 +6,8 @@
+ #define __CPROVER_STDIO_H_INCLUDED
+ #endif
+
+-/* undefine macros in OpenBSD's stdio.h that are problematic to the checker. */
+-#if defined(__OpenBSD__)
++/* undefine macros in FreeBSD's and OpenBSD's stdio.h that are problematic to the checker. */
++#if defined(__FreeBSD__) || defined(__OpenBSD__)
+ #undef getchar
+ #undef putchar
+ #undef getc
diff --git a/devel/cbmc/pkg-plist b/devel/cbmc/pkg-plist
index 2d23b585ef57..65eae537b7f4 100644
--- a/devel/cbmc/pkg-plist
+++ b/devel/cbmc/pkg-plist
@@ -1,23 +1,30 @@
bin/cbmc
+bin/cprover
bin/crangler
bin/goto-analyzer
bin/goto-cc
bin/goto-diff
-bin/goto-instrument
-bin/goto-inspect
+bin/goto-gcc
bin/goto-harness
+bin/goto-inspect
+bin/goto-instrument
+bin/goto-ld
bin/goto-synthesizer
-bin/symtab2gb
bin/ls_parse.py
-bin/goto-gcc
-bin/goto-ld
+bin/symtab2gb
+etc/bash_completion.d/cbmc
+include/cprover/api.h
+include/cprover/api_options.h
+include/cprover/verification_result.h
+lib/libcprover.6.9.0.a
share/man/man1/cbmc.1.gz
share/man/man1/crangler.1.gz
share/man/man1/goto-analyzer.1.gz
share/man/man1/goto-cc.1.gz
share/man/man1/goto-diff.1.gz
+share/man/man1/goto-gcc.1.gz
share/man/man1/goto-harness.1.gz
-share/man/man1/goto-inspect.1.gz
share/man/man1/goto-instrument.1.gz
+share/man/man1/goto-ld.1.gz
share/man/man1/goto-synthesizer.1.gz
share/man/man1/symtab2gb.1.gz