From nobody Thu Feb 01 17:55:09 2024 X-Original-To: dev-commits-ports-main@mlmmj.nyi.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2610:1c1:1:606c::19:1]) by mlmmj.nyi.freebsd.org (Postfix) with ESMTP id 4TQmlL1ynNz58L2q; Thu, 1 Feb 2024 17:55:10 +0000 (UTC) (envelope-from git@FreeBSD.org) Received: from mxrelay.nyi.freebsd.org (mxrelay.nyi.freebsd.org [IPv6:2610:1c1:1:606c::19:3]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256 client-signature RSA-PSS (4096 bits) client-digest SHA256) (Client CN "mxrelay.nyi.freebsd.org", Issuer "R3" (verified OK)) by mx1.freebsd.org (Postfix) with ESMTPS id 4TQmlL1dXGz47ZN; Thu, 1 Feb 2024 17:55:10 +0000 (UTC) (envelope-from git@FreeBSD.org) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1706810110; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding; bh=+sAx1GO1HD6CKQrEnKIdp9GVR+UmxwXWFTchuAeAXFQ=; b=LLR1NBzR26yWrzQxZZdz9EA+66S+h395fWheJpEof1S4PiF8G6vS73Q1mr77zTkbWW/YS1 PEIq7O37ost1FwLEZHfShWgroYw1rwSfy4VWL9Pv4apprEZALuIORZfTNYOi5OHpVG9Jfo 0NC/DVoBTA5PlkUBPuygV4TZzaWRq3WvbGifw/ahPdHvr597K+N3lzWt78z5bDFbOuvz/D UnNgeHVjR9tYBox3s5OgITuJb+fBDFL7RzvzIIWZh6p3pfEKerdqlPmpfPkw37xQ/2kFGf 4Hn3LETF7RFMkfQQoecjGcnNfXK4lh6y0fB3HaktZQeJk+fJ3LaxevkYqS+a5g== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1706810110; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding; bh=+sAx1GO1HD6CKQrEnKIdp9GVR+UmxwXWFTchuAeAXFQ=; b=qqtK2MnBhDlaWzluMRTDJoJt33TvbkU+FD48VPw6AU+lJupSC1fbfugza4fTP81KSoUQqY AaJ0EPUuG6Mk/drSlni5oRK2GUrXZpZQDgsV5CdI35X4Gn4JEfzIPNyIkKA0CziUDj2qkT UbQlzVaA5WKIUEYFVLpIM/0in+FPGxth+qoLsTtpyoK+nbwXVfaeGPVwb5BDw/zTvfLs6S hrJlIENLo3UjQa/1DOkw1PCrLEk8LkJdRsCJGX5hUxL+qT3kBVZqvz8srDzVm9DB6wxVVF Bn4GD27SyOlf+LSDd6KcjRmlrWO02X3vNT7hsSUQxek4oCkhbzsi3wr2aiPECg== ARC-Authentication-Results: i=1; mx1.freebsd.org; none ARC-Seal: i=1; s=dkim; d=freebsd.org; t=1706810110; a=rsa-sha256; cv=none; b=yh+f4Kt7oNQ6g61PKEt5eLtJEHHrqtRhLe1p7wTgIF+35ah9nqU+OAEt3gj+TLqqcmA9pt jSYuIp5f/y/lk43U9dv+M8ZzkYzkg0YMCz/kf3ASch6pvV6idaYoc4WS3mSD7XxcEMa4jM pkmIAi4X8Y1244x9FmGhkC6SjAqxLbc0K6tXRDWAjR9Puj3s4Nb5ZMI7fovMQIB6eoUS25 W15yxR4RmzqQB2+Iy0bNj2Akr7Kh85/PynvqOwcQIkGEQSu+js+nZl43rNoIdamMoonYeo d9u6ngfmwE+DHmI+JCfxTr3JSWKhcS/u2l6Qkre5HU6yMWGVAu9b1btz3y0iBg== Received: from gitrepo.freebsd.org (gitrepo.freebsd.org [IPv6:2610:1c1:1:6068::e6a:5]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (Client did not present a certificate) by mxrelay.nyi.freebsd.org (Postfix) with ESMTPS id 4TQmlL0bs2z1Bmm; Thu, 1 Feb 2024 17:55:10 +0000 (UTC) (envelope-from git@FreeBSD.org) Received: from gitrepo.freebsd.org ([127.0.1.44]) by gitrepo.freebsd.org (8.17.1/8.17.1) with ESMTP id 411Ht9u9016152; Thu, 1 Feb 2024 17:55:09 GMT (envelope-from git@gitrepo.freebsd.org) Received: (from git@localhost) by gitrepo.freebsd.org (8.17.1/8.17.1/Submit) id 411Ht9G8016149; Thu, 1 Feb 2024 17:55:09 GMT (envelope-from git) Date: Thu, 1 Feb 2024 17:55:09 GMT Message-Id: <202402011755.411Ht9G8016149@gitrepo.freebsd.org> To: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org From: Olivier Cochard Subject: git: 7f087b720e52 - main - devel/cbmc: add new port List-Id: Commits to the main branch of the FreeBSD ports repository List-Archive: https://lists.freebsd.org/archives/dev-commits-ports-main List-Help: List-Post: List-Subscribe: List-Unsubscribe: Sender: owner-dev-commits-ports-main@freebsd.org X-BeenThere: dev-commits-ports-main@freebsd.org MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Git-Committer: olivier X-Git-Repository: ports X-Git-Refname: refs/heads/main X-Git-Reftype: branch X-Git-Commit: 7f087b720e52d51b22db0da2d7565418a0e428ef Auto-Submitted: auto-generated The branch main has been updated by olivier: URL: https://cgit.FreeBSD.org/ports/commit/?id=7f087b720e52d51b22db0da2d7565418a0e428ef commit 7f087b720e52d51b22db0da2d7565418a0e428ef Author: Olivier Cochard AuthorDate: 2024-02-01 17:50:02 +0000 Commit: Olivier Cochard CommitDate: 2024-02-01 17:53:55 +0000 devel/cbmc: add new port Bounded Model Checker for C and C++ programs https://github.com/diffblue/cbmc Sponsored by: Netflix --- devel/Makefile | 1 + devel/cbmc/Makefile | 46 +++++++++++++++++ devel/cbmc/distinfo | 5 ++ .../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_common | 11 ++++ .../files/patch-src_solvers_sat_external__sat.cpp | 13 +++++ devel/cbmc/files/patch-src_util_optional.h | 29 +++++++++++ devel/cbmc/pkg-descr | 7 +++ devel/cbmc/pkg-plist | 23 +++++++++ 18 files changed, 387 insertions(+) diff --git a/devel/Makefile b/devel/Makefile index 4da71e0953a1..51481c8a3aca 100644 --- a/devel/Makefile +++ b/devel/Makefile @@ -351,6 +351,7 @@ SUBDIR += catch2 SUBDIR += cbang SUBDIR += cbfmt + SUBDIR += cbmc SUBDIR += cbrowser SUBDIR += cc65 SUBDIR += ccache diff --git a/devel/cbmc/Makefile b/devel/cbmc/Makefile new file mode 100644 index 000000000000..c7f7b3650e63 --- /dev/null +++ b/devel/cbmc/Makefile @@ -0,0 +1,46 @@ +PORTNAME= cbmc +PORTVERSION= 5.95.1 +DISTVERSIONPREFIX= cbmc- +CATEGORIES= devel +MASTER_SITES= DEBIAN/pool/main/m/minisat2:minisat +DISTFILES= minisat2_2.2.1.orig.tar.gz:minisat + +MAINTAINER= olivier@FreeBSD.org +COMMENT= Bounded Model Checker for C and C++ programs +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 + +USES= gmake bison python shebangfix + +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/ + +.include diff --git a/devel/cbmc/distinfo b/devel/cbmc/distinfo new file mode 100644 index 000000000000..f3e6d1161c6a --- /dev/null +++ b/devel/cbmc/distinfo @@ -0,0 +1,5 @@ +TIMESTAMP = 1706723199 +SHA256 (minisat2_2.2.1.orig.tar.gz) = e54afa3c192c1753bc8075c0c7e126d5c495d9066e3f90a2588091149ac9ca40 +SIZE (minisat2_2.2.1.orig.tar.gz) = 44229 +SHA256 (diffblue-cbmc-cbmc-5.95.1_GH0.tar.gz) = fdc1e862752430f8d069eb2f9c33dcd05078cf955bbc900e2cc840bcb01b3783 +SIZE (diffblue-cbmc-cbmc-5.95.1_GH0.tar.gz) = 9073428 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 new file mode 100644 index 000000000000..c15c2f12fb0a --- /dev/null +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_Solver.cc @@ -0,0 +1,20 @@ +--- 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 new file mode 100644 index 000000000000..fa26c6372b36 --- /dev/null +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_SolverTypes.h @@ -0,0 +1,59 @@ +--- 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 ++#include + union { Lit lit; float act; uint32_t abs; CRef rel; } data[0]; ++#include + + 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 new file mode 100644 index 000000000000..d8c9ddedb701 --- /dev/null +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h @@ -0,0 +1,12 @@ +--- 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 ++#ifndef _MSC_VER + # include ++#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 new file mode 100644 index 000000000000..b3062972c5c9 --- /dev/null +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_Vec.h @@ -0,0 +1,16 @@ +--- 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::capacity(int min_cap) { + void vec::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 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 new file mode 100644 index 000000000000..8c8b9680bf6d --- /dev/null +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_XAlloc.h @@ -0,0 +1,19 @@ +--- 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 + #include + + 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 new file mode 100644 index 000000000000..c83101829f03 --- /dev/null +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_simp_SimpSolver.cc @@ -0,0 +1,37 @@ +--- 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& 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 new file mode 100644 index 000000000000..84b5f289e8a5 --- /dev/null +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_Options.cc @@ -0,0 +1,15 @@ +--- 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 new file mode 100644 index 000000000000..c844c16940d9 --- /dev/null +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_Options.h @@ -0,0 +1,30 @@ +--- 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 new file mode 100644 index 000000000000..a0b231103805 --- /dev/null +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_ParseUtils.h @@ -0,0 +1,33 @@ +--- 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 + #include + +-#include ++//#include + + 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 new file mode 100644 index 000000000000..a49382def0dc --- /dev/null +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_System.h @@ -0,0 +1,11 @@ +--- 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 + #endif + diff --git a/devel/cbmc/files/patch-src_common b/devel/cbmc/files/patch-src_common new file mode 100644 index 000000000000..6944a39d7788 --- /dev/null +++ b/devel/cbmc/files/patch-src_common @@ -0,0 +1,11 @@ +--- src/common.orig 2024-02-01 00:44:35 UTC ++++ src/common +@@ -64,7 +64,7 @@ else ifeq ($(filter-out FreeBSD,$(BUILD_ENV_)),) + YFLAGS ?= -v + else ifeq ($(filter-out FreeBSD,$(BUILD_ENV_)),) + CP_CXXFLAGS += +- LINKLIB = ar rcT $@ $^ ++ LINKLIB = llvm-ar rcT $@ $^ + LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS) + LINKNATIVE = $(HOSTCXX) $(HOSTLINKFLAGS) -o $@ $^ + ifeq ($(origin CC),default) diff --git a/devel/cbmc/files/patch-src_solvers_sat_external__sat.cpp b/devel/cbmc/files/patch-src_solvers_sat_external__sat.cpp new file mode 100644 index 000000000000..f0dd61cd9963 --- /dev/null +++ b/devel/cbmc/files/patch-src_solvers_sat_external__sat.cpp @@ -0,0 +1,13 @@ +--- src/solvers/sat/external_sat.cpp.orig 2023-10-30 12:11:18 UTC ++++ src/solvers/sat/external_sat.cpp +@@ -119,8 +119,8 @@ external_satt::resultt external_satt::parse_result(std + { + try + { +- signed long long as_long = std::stol(assignment_string); +- size_t index = std::labs(as_long); ++ signed long long as_long = std::stoll(assignment_string); ++ size_t index = std::llabs(as_long); + + if(index >= number_of_variables) + { diff --git a/devel/cbmc/files/patch-src_util_optional.h b/devel/cbmc/files/patch-src_util_optional.h new file mode 100644 index 000000000000..4507ce0ade2b --- /dev/null +++ b/devel/cbmc/files/patch-src_util_optional.h @@ -0,0 +1,29 @@ +--- src/util/optional.h.orig 2023-10-30 12:11:18 UTC ++++ src/util/optional.h +@@ -11,20 +11,20 @@ Author: Diffblue Ltd. + #define CPROVER_UTIL_OPTIONAL_H + + #if defined __clang__ +- #pragma clang diagnostic push ignore "-Wall" +- #pragma clang diagnostic push ignore "-Wpedantic" ++ #pragma clang diagnostic push ++ #pragma clang diagnostic ignored "-Wall" ++ #pragma clang diagnostic ignored "-Wpedantic" + #elif defined __GNUC__ +- #pragma GCC diagnostic push ignore "-Wall" +- #pragma GCC diagnostic push ignore "-Wpedantic" ++ #pragma GCC diagnostic push ++ #pragma GCC diagnostic ignored "-Wall" ++ #pragma GCC diagnostic ignored "-Wpedantic" + #elif defined _MSC_VER + #pragma warning(push) + #endif + #include + #if defined __clang__ + #pragma clang diagnostic pop +- #pragma clang diagnostic pop + #elif defined __GNUC__ +- #pragma GCC diagnostic pop + #pragma GCC diagnostic pop + #elif defined _MSC_VER + #pragma warning(pop) diff --git a/devel/cbmc/pkg-descr b/devel/cbmc/pkg-descr new file mode 100644 index 000000000000..2004194d7c43 --- /dev/null +++ b/devel/cbmc/pkg-descr @@ -0,0 +1,7 @@ +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 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. diff --git a/devel/cbmc/pkg-plist b/devel/cbmc/pkg-plist new file mode 100644 index 000000000000..2d23b585ef57 --- /dev/null +++ b/devel/cbmc/pkg-plist @@ -0,0 +1,23 @@ +bin/cbmc +bin/crangler +bin/goto-analyzer +bin/goto-cc +bin/goto-diff +bin/goto-instrument +bin/goto-inspect +bin/goto-harness +bin/goto-synthesizer +bin/symtab2gb +bin/ls_parse.py +bin/goto-gcc +bin/goto-ld +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-harness.1.gz +share/man/man1/goto-inspect.1.gz +share/man/man1/goto-instrument.1.gz +share/man/man1/goto-synthesizer.1.gz +share/man/man1/symtab2gb.1.gz