Date: Sat, 20 Jun 2026 20:53:42 +0000 From: Olivier Cochard <olivier@FreeBSD.org> To: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org Subject: git: 85f08f2fd423 - main - devel/cbmc: witch to the recommended cmake build and add test support Message-ID: <6a36fdd6.3eb53.5953172f@gitrepo.freebsd.org>
index | next in thread | raw e-mail
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.gzhome | help
Want to link to this message? Use this
URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?6a36fdd6.3eb53.5953172f>