Date: Fri, 02 Feb 2024 01:05:00 +0100 From: Daniel Engberg <daniel.engberg.lists@pyret.net> To: Olivier Cochard <olivier@FreeBSD.org> Cc: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org Subject: Re: git: 7f087b720e52 - main - devel/cbmc: add new port Message-ID: <379c7ddb410058469dcda4f67b45caa9@mail.infomaniak.com> In-Reply-To: <202402011755.411Ht9G8016149@gitrepo.freebsd.org>
index | next in thread | previous in thread | raw e-mail
[-- Attachment #1 --] On 2024-02-01T18:55:09.000+01:00, Olivier Cochard <olivier@FreeBSD.org> wrote: > The branch main has been updated by olivier: > > URL: https://cgit.FreeBSD.org/ports/commit/?id=7f087b720e52d51b22db0da2d7565418a0e428ef > > commit 7f087b720e52d51b22db0da2d7565418a0e428ef > > Author: Olivier Cochard <olivier@FreeBSD.org> > > AuthorDate: 2024-02-01 17:50:02 +0000 > > Commit: Olivier Cochard <olivier@FreeBSD.org> > > 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 [http://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 [http://SimpSolver.cc] | 37 ++++++++++++++ > > .../patch-minisat-2.2.1_minisat_utils_Options.cc [http://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 [http://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 [http://parse.py] ${STAGEDIR}${PREFIX}/bin/ > > + > > +.include <bsd.port.mk> [http://bsd.port.mk>]; > > 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 [http://Solver.cc] b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_Solver.cc [http://Solver.cc] > > new file mode 100644 > > index 000000000000..c15c2f12fb0a > > --- /dev/null > > +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_Solver.cc [http://Solver.cc] > > @@ -0,0 +1,20 @@ > > +--- minisat-2.2.1/minisat/core/Solver.cc.orig [http://Solver.cc.orig] 2011-02-21 13:31:17 UTC > > ++++ minisat-2.2.1/minisat/core/Solver.cc [http://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 <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] [http://from.data[header.size]].act; > > + else > > + data[header.size].abs = from.data[header.size] [http://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 <stdint.h> > > ++#ifndef _MSC_VER > > + # include <inttypes.h> > > ++#endif > > + > > + The branch main has been updated by olivier: > > URL: https://cgit.FreeBSD.org/ports/commit/?id=7f087b720e52d51b22db0da2d7565418a0e428ef > > commit 7f087b720e52d51b22db0da2d7565418a0e428ef > > Author: Olivier Cochard <olivier@FreeBSD.org> > > AuthorDate: 2024-02-01 17:50:02 +0000 > > Commit: Olivier Cochard <olivier@FreeBSD.org> > > 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 [http://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 [http://SimpSolver.cc] | 37 ++++++++++++++ > > .../patch-minisat-2.2.1_minisat_utils_Options.cc [http://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 [http://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 [http://parse.py] ${STAGEDIR}${PREFIX}/bin/ > > + > > +.include <bsd.port.mk> [http://bsd.port.mk>]; > > 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 [http://Solver.cc] b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_Solver.cc [http://Solver.cc] > > new file mode 100644 > > index 000000000000..c15c2f12fb0a > > --- /dev/null > > +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_Solver.cc [http://Solver.cc] > > @@ -0,0 +1,20 @@ > > +--- minisat-2.2.1/minisat/core/Solver.cc.orig [http://Solver.cc.orig] 2011-02-21 13:31:17 UTC > > ++++ minisat-2.2.1/minisat/core/Solver.cc [http://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 <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] [http://from.data[header.size]].act; > > + else > > + data[header.size].abs = from.data[header.size] [http://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 <stdint.h> > > ++#ifndef _MSC_VER > > + # include <inttypes.h> > > ++#endif > > + > > + #endiffile 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 <nonstd/optional.hpp> > > + #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 [http://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 Hi, Are these patches upstreamed or backported? Best regards, Daniel (diizzy@) [-- Attachment #2 --] <div>On 2024-02-01T18:55:09.000+01:00, Olivier Cochard <olivier@FreeBSD.org> wrote:<br></div><div class="ik_mail_quote answerContentMessage"><blockquote class="ws-ng-quote"><pre style="white-space: normal;"><div>The branch main has been updated by olivier:<br></div><div><br></div><div>URL: <a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="https://cgit.FreeBSD.org/ports/commit/?id=7f087b720e52d51b22db0da2d7565418a0e428ef" target="_blank">https://cgit.FreeBSD.org/ports/commit/?id=7f087b720e52d51b22db0da2d7565418a0e428ef</a><br></div><div><br></div><div>commit 7f087b720e52d51b22db0da2d7565418a0e428ef<br></div><div>Author: Olivier Cochard <<a class="defaultMailLink" href="mailto:olivier@FreeBSD.org">olivier@FreeBSD.org</a>><br></div><div>AuthorDate: 2024-02-01 17:50:02 +0000<br></div><div>Commit: Olivier Cochard <<a class="defaultMailLink" href="mailto:olivier@FreeBSD.org">olivier@FreeBSD.org</a>><br></div><div>CommitDate: 2024-02-01 17:53:55 +0000<br></div><div><br></div><div> devel/cbmc: add new port<br></div><div> <br></div><div> Bounded Model Checker for C and C++ programs<br></div><div> <a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="https://github.com/diffblue/cbmc" target="_blank">https://github.com/diffblue/cbmc</a><br></div><div>; <br></div><div> Sponsored by: Netflix<br></div><div>---<br></div><div> devel/Makefile | 1 +<br></div><div> devel/cbmc/Makefile | 46 +++++++++++++++++<br></div><div> devel/cbmc/distinfo | 5 ++<br></div><div> .../patch-minisat-2.2.1_minisat_core_<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://Solver.cc" target="_blank">Solver.cc</a> | 20 ++++++++<br></div><div> .../patch-minisat-2.2.1_minisat_core_SolverTypes.h | 59 ++++++++++++++++++++++<br></div><div> .../patch-minisat-2.2.1_minisat_mtl_IntTypes.h | 12 +++++<br></div><div> .../files/patch-minisat-2.2.1_minisat_mtl_Vec.h | 16 ++++++<br></div><div> .../files/patch-minisat-2.2.1_minisat_mtl_XAlloc.h | 19 +++++++<br></div><div> .../patch-minisat-2.2.1_minisat_simp_<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://SimpSolver.cc" target="_blank">SimpSolver.cc</a> | 37 ++++++++++++++<br></div><div> .../patch-minisat-2.2.1_minisat_utils_<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://Options.cc" target="_blank">Options.cc</a> | 15 ++++++<br></div><div> .../patch-minisat-2.2.1_minisat_utils_Options.h | 30 +++++++++++<br></div><div> .../patch-minisat-2.2.1_minisat_utils_ParseUtils.h | 33 ++++++++++++<br></div><div> .../patch-minisat-2.2.1_minisat_utils_System.h | 11 ++++<br></div><div> devel/cbmc/files/patch-src_common | 11 ++++<br></div><div> .../files/patch-src_solvers_sat_external__sat.cpp | 13 +++++<br></div><div> devel/cbmc/files/patch-src_util_optional.h | 29 +++++++++++<br></div><div> devel/cbmc/pkg-descr | 7 +++<br></div><div> devel/cbmc/pkg-plist | 23 +++++++++<br></div><div> 18 files changed, 387 insertions(+)<br></div><div><br></div><div>diff --git a/devel/Makefile b/devel/Makefile<br></div><div>index 4da71e0953a1..51481c8a3aca 100644<br></div><div>--- a/devel/Makefile<br></div><div>+++ b/devel/Makefile<br></div><div>@@ -351,6 +351,7 @@<br></div><div> SUBDIR += catch2<br></div><div> SUBDIR += cbang<br></div><div> SUBDIR += cbfmt<br></div><div>+ SUBDIR += cbmc<br></div><div> SUBDIR += cbrowser<br></div><div> SUBDIR += cc65<br></div><div> SUBDIR += ccache<br></div><div>diff --git a/devel/cbmc/Makefile b/devel/cbmc/Makefile<br></div><div>new file mode 100644<br></div><div>index 000000000000..c7f7b3650e63<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/Makefile<br></div><div>@@ -0,0 +1,46 @@<br></div><div>+PORTNAME= cbmc<br></div><div>+PORTVERSION= 5.95.1<br></div><div>+DISTVERSIONPREFIX= cbmc-<br></div><div>+CATEGORIES= devel<br></div><div>+MASTER_SITES= DEBIAN/pool/main/m/minisat2:minisat<br></div><div>+DISTFILES= minisat2_2.2.1.orig.tar.gz:minisat<br></div><div>+<br></div><div>+MAINTAINER= <a class="defaultMailLink" href="mailto:olivier@FreeBSD.org">olivier@FreeBSD.org</a><br></div><div>+COMMENT= Bounded Model Checker for C and C++ programs<br></div><div>+WWW= <a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="https://github.com/diffblue/cbmc" target="_blank">https://github.com/diffblue/cbmc</a><br></div><div>+<br></div><div>+LICENSE= BSD4CLAUSE<br></div><div>+LICENSE_FILE= ${WRKSRC}/LICENSE<br></div><div>+<br></div><div>+BUILD_DEPENDS= ${LOCALBASE}/bin/flex:textproc/flex<br></div><div>+RUN_DEPENDS= ${LOCALBASE}/bin/cvc5:math/cvc5 \<br></div><div>+ ${LOCALBASE}/bin/z3:math/z3<br></div><div>+<br></div><div>+USES= gmake bison python shebangfix<br></div><div>+<br></div><div>+USE_GITHUB= yes<br></div><div>+GH_ACCOUNT= diffblue<br></div><div>+SHEBANG_FILES= ${WRKSRC}/scripts/ls_<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://parse.py" target="_blank">parse.py</a><br></div><div>+WRKSRC_minisat= ${WRKDIR}/minisat2-2.2.1<br></div><div>+<br></div><div>+post-patch:<br></div><div>+ @${REINPLACE_CMD} -e 's|.*git describe --tags.*|GIT_INFO = ${PORTNAME}-${PORTVERSION}|' \<br></div><div>+ ${WRKSRC}/src/util/Makefile<br></div><div>+post-extract:<br></div><div>+ @${MV} ${WRKSRC_minisat} ${WRKSRC}/minisat-2.2.1<br></div><div>+<br></div><div>+do-build:<br></div><div>+ @${MKDIR} ${STAGEDIR}<br></div><div>+ cd ${WRKSRC} && ${GMAKE} -C src -j${MAKE_JOBS_NUMBER}<br></div><div>+<br></div><div>+do-install:<br></div><div>+. for x in cbmc crangler goto-analyzer goto-cc goto-diff goto-instrument \<br></div><div>+ goto-inspect goto-harness goto-synthesizer symtab2gb<br></div><div>+ ${INSTALL_PROGRAM} ${WRKSRC}/src/${x}/${x} ${STAGEDIR}${PREFIX}/bin/<br></div><div>+ ${INSTALL_MAN} ${WRKSRC}/doc/man/${x}.1 ${STAGEDIR}${PREFIX}/share/man/man1/<br></div><div>+. endfor<br></div><div>+ ${LN} -sf goto-cc ${STAGEDIR}${PREFIX}/bin/goto-gcc<br></div><div>+ ${LN} -sf goto-cc ${STAGEDIR}${PREFIX}/bin/goto-ld<br></div><div>+ ${INSTALL_SCRIPT} ${WRKSRC}/scripts/ls_<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://parse.py" target="_blank">parse.py</a> ${STAGEDIR}${PREFIX}/bin/<br></div><div>+<br></div><div>+.include <<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://bsd.port.mk>" target="_blank">bsd.port.mk></a>;<br></div><div>diff --git a/devel/cbmc/distinfo b/devel/cbmc/distinfo<br></div><div>new file mode 100644<br></div><div>index 000000000000..f3e6d1161c6a<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/distinfo<br></div><div>@@ -0,0 +1,5 @@<br></div><div>+TIMESTAMP = 1706723199<br></div><div>+SHA256 (minisat2_2.2.1.orig.tar.gz) = e54afa3c192c1753bc8075c0c7e126d5c495d9066e3f90a2588091149ac9ca40<br></div><div>+SIZE (minisat2_2.2.1.orig.tar.gz) = 44229<br></div><div>+SHA256 (diffblue-cbmc-cbmc-5.95.1_GH0.tar.gz) = fdc1e862752430f8d069eb2f9c33dcd05078cf955bbc900e2cc840bcb01b3783<br></div><div>+SIZE (diffblue-cbmc-cbmc-5.95.1_GH0.tar.gz) = 9073428<br></div><div>diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://Solver.cc" target="_blank">Solver.cc</a> b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://Solver.cc" target="_blank">Solver.cc</a><br></div><div>new file mode 100644<br></div><div>index 000000000000..c15c2f12fb0a<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://Solver.cc" target="_blank">Solver.cc</a><br></div><div>@@ -0,0 +1,20 @@<br></div><div>+--- minisat-2.2.1/minisat/core/<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://Solver.cc.orig" target="_blank">Solver.cc.orig</a> 2011-02-21 13:31:17 UTC<br></div><div>++++ minisat-2.2.1/minisat/core/<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://Solver.cc" target="_blank">Solver.cc</a><br></div><div>+@@ -210,7 +210,7 @@ void Solver::cancelUntil(int level) {<br></div><div>+ for (int c = trail.size()-1; c &gt;= trail_lim[level]; c--){<br></div><div>+ Var x = var(trail[c]);<br></div><div>+ assigns [x] = l_Undef;<br></div><div>+- if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())<br></div><div>++ if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last()))<br></div><div>+ polarity[x] = sign(trail[c]);<br></div><div>+ insertVarOrder(x); }<br></div><div>+ qhead = trail_lim[level];<br></div><div>+@@ -666,7 +666,7 @@ lbool Solver::search(int nof_conflicts)<br></div><div>+ <br></div><div>+ }else{<br></div><div>+ // NO CONFLICT<br></div><div>+- if (nof_conflicts &gt;= 0 && conflictC &gt;= nof_conflicts || !withinBudget()){<br></div><div>++ if ((nof_conflicts &gt;= 0 && conflictC &gt;= nof_conflicts) || !withinBudget()){<br></div><div>+ // Reached bound on number of conflicts:<br></div><div>+ progress_estimate = progressEstimate();<br></div><div>+ cancelUntil(0);<br></div><div>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<br></div><div>new file mode 100644<br></div><div>index 000000000000..fa26c6372b36<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_SolverTypes.h<br></div><div>@@ -0,0 +1,59 @@<br></div><div>+--- minisat-2.2.1/minisat/core/SolverTypes.h.orig 2011-02-21 13:31:17 UTC<br></div><div>++++ minisat-2.2.1/minisat/core/SolverTypes.h<br></div><div>+@@ -47,7 +47,7 @@ struct Lit {<br></div><div>+ int x;<br></div><div>+ <br></div><div>+ // Use this as a constructor:<br></div><div>+- friend Lit mkLit(Var var, bool sign = false);<br></div><div>++ //friend Lit mkLit(Var var, bool sign = false);<br></div><div>+ <br></div><div>+ bool operator == (Lit p) const { return x == p.x; }<br></div><div>+ bool operator != (Lit p) const { return x != p.x; }<br></div><div>+@@ -55,7 +55,7 @@ struct Lit {<br></div><div>+ };<br></div><div>+ <br></div><div>+ <br></div><div>+-inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }<br></div><div>++inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; }<br></div><div>+ inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; }<br></div><div>+ inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; }<br></div><div>+ inline bool sign (Lit p) { return p.x & 1; }<br></div><div>+@@ -127,7 +127,10 @@ class Clause {<br></div><div>+ unsigned has_extra : 1;<br></div><div>+ unsigned reloced : 1;<br></div><div>+ unsigned size : 27; } header;<br></div><div>++#include <util/pragma_push.def><br></div><div>++#include <util/pragma_wzero_length_array.def><br></div><div>+ union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];<br></div><div>++#include <util/pragma_pop.def><br></div><div>+ <br></div><div>+ friend class ClauseAllocator;<br></div><div>+ <br></div><div>+@@ -142,11 +145,12 @@ class Clause {<br></div><div>+ for (int i = 0; i < ps.size(); i++) <br></div><div>+ data[i].lit = ps[i];<br></div><div>+ <br></div><div>+- if (header.has_extra)<br></div><div>++ if (header.has_extra) {<br></div><div>+ if (header.learnt)<br></div><div>+ data[header.size].act = 0;<br></div><div>+ else<br></div><div>+ calcAbstraction();<br></div><div>++ }<br></div><div>+ }<br></div><div>+ <br></div><div>+ // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).<br></div><div>+@@ -157,11 +161,12 @@ class Clause {<br></div><div>+ for (int i = 0; i < from.size(); i++)<br></div><div>+ data[i].lit = from[i];<br></div><div>+ <br></div><div>+- if (header.has_extra)<br></div><div>++ if (header.has_extra) {<br></div><div>+ if (header.learnt)<br></div><div>+ data[header.size].act = <a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://from.data[header.size]" target="_blank">from.data[header.size]</a>.act;<br></div><div>+ else <br></div><div>+ data[header.size].abs = <a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://from.data[header.size]" target="_blank">from.data[header.size]</a>.abs;<br></div><div>++ }<br></div><div>+ }<br></div><div>+ <br></div><div>+ public:<br></div><div>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<br></div><div>new file mode 100644<br></div><div>index 000000000000..d8c9ddedb701<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h<br></div><div>@@ -0,0 +1,12 @@<br></div><div>+--- minisat-2.2.1/minisat/mtl/IntTypes.h.orig 2011-02-21 13:31:17 UTC<br></div><div>++++ minisat-2.2.1/minisat/mtl/IntTypes.h<br></div><div>+@@ -31,7 +31,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OT<br></div><div>+ #else<br></div><div>+ <br></div><div>+ # include <stdint.h><br></div><div>++#ifndef _MSC_VER<br></div><div>+ # include <inttypes.h><br></div><div>++#endif<br></div><div>+ <br></div><div>+ The branch main has been updated by olivier:<br></div><div><br></div><div>URL: <a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="https://cgit.FreeBSD.org/ports/commit/?id=7f087b720e52d51b22db0da2d7565418a0e428ef" target="_blank">https://cgit.FreeBSD.org/ports/commit/?id=7f087b720e52d51b22db0da2d7565418a0e428ef</a><br></div><div><br></div><div>commit 7f087b720e52d51b22db0da2d7565418a0e428ef<br></div><div>Author: Olivier Cochard <<a class="defaultMailLink" href="mailto:olivier@FreeBSD.org">olivier@FreeBSD.org</a>><br></div><div>AuthorDate: 2024-02-01 17:50:02 +0000<br></div><div>Commit: Olivier Cochard <<a class="defaultMailLink" href="mailto:olivier@FreeBSD.org">olivier@FreeBSD.org</a>><br></div><div>CommitDate: 2024-02-01 17:53:55 +0000<br></div><div><br></div><div> devel/cbmc: add new port<br></div><div> <br></div><div> Bounded Model Checker for C and C++ programs<br></div><div> <a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="https://github.com/diffblue/cbmc" target="_blank">https://github.com/diffblue/cbmc</a><br></div><div>; <br></div><div> Sponsored by: Netflix<br></div><div>---<br></div><div> devel/Makefile | 1 +<br></div><div> devel/cbmc/Makefile | 46 +++++++++++++++++<br></div><div> devel/cbmc/distinfo | 5 ++<br></div><div> .../patch-minisat-2.2.1_minisat_core_<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://Solver.cc" target="_blank">Solver.cc</a> | 20 ++++++++<br></div><div> .../patch-minisat-2.2.1_minisat_core_SolverTypes.h | 59 ++++++++++++++++++++++<br></div><div> .../patch-minisat-2.2.1_minisat_mtl_IntTypes.h | 12 +++++<br></div><div> .../files/patch-minisat-2.2.1_minisat_mtl_Vec.h | 16 ++++++<br></div><div> .../files/patch-minisat-2.2.1_minisat_mtl_XAlloc.h | 19 +++++++<br></div><div> .../patch-minisat-2.2.1_minisat_simp_<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://SimpSolver.cc" target="_blank">SimpSolver.cc</a> | 37 ++++++++++++++<br></div><div> .../patch-minisat-2.2.1_minisat_utils_<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://Options.cc" target="_blank">Options.cc</a> | 15 ++++++<br></div><div> .../patch-minisat-2.2.1_minisat_utils_Options.h | 30 +++++++++++<br></div><div> .../patch-minisat-2.2.1_minisat_utils_ParseUtils.h | 33 ++++++++++++<br></div><div> .../patch-minisat-2.2.1_minisat_utils_System.h | 11 ++++<br></div><div> devel/cbmc/files/patch-src_common | 11 ++++<br></div><div> .../files/patch-src_solvers_sat_external__sat.cpp | 13 +++++<br></div><div> devel/cbmc/files/patch-src_util_optional.h | 29 +++++++++++<br></div><div> devel/cbmc/pkg-descr | 7 +++<br></div><div> devel/cbmc/pkg-plist | 23 +++++++++<br></div><div> 18 files changed, 387 insertions(+)<br></div><div><br></div><div>diff --git a/devel/Makefile b/devel/Makefile<br></div><div>index 4da71e0953a1..51481c8a3aca 100644<br></div><div>--- a/devel/Makefile<br></div><div>+++ b/devel/Makefile<br></div><div>@@ -351,6 +351,7 @@<br></div><div> SUBDIR += catch2<br></div><div> SUBDIR += cbang<br></div><div> SUBDIR += cbfmt<br></div><div>+ SUBDIR += cbmc<br></div><div> SUBDIR += cbrowser<br></div><div> SUBDIR += cc65<br></div><div> SUBDIR += ccache<br></div><div>diff --git a/devel/cbmc/Makefile b/devel/cbmc/Makefile<br></div><div>new file mode 100644<br></div><div>index 000000000000..c7f7b3650e63<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/Makefile<br></div><div>@@ -0,0 +1,46 @@<br></div><div>+PORTNAME= cbmc<br></div><div>+PORTVERSION= 5.95.1<br></div><div>+DISTVERSIONPREFIX= cbmc-<br></div><div>+CATEGORIES= devel<br></div><div>+MASTER_SITES= DEBIAN/pool/main/m/minisat2:minisat<br></div><div>+DISTFILES= minisat2_2.2.1.orig.tar.gz:minisat<br></div><div>+<br></div><div>+MAINTAINER= <a class="defaultMailLink" href="mailto:olivier@FreeBSD.org">olivier@FreeBSD.org</a><br></div><div>+COMMENT= Bounded Model Checker for C and C++ programs<br></div><div>+WWW= <a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="https://github.com/diffblue/cbmc" target="_blank">https://github.com/diffblue/cbmc</a><br></div><div>+<br></div><div>+LICENSE= BSD4CLAUSE<br></div><div>+LICENSE_FILE= ${WRKSRC}/LICENSE<br></div><div>+<br></div><div>+BUILD_DEPENDS= ${LOCALBASE}/bin/flex:textproc/flex<br></div><div>+RUN_DEPENDS= ${LOCALBASE}/bin/cvc5:math/cvc5 \<br></div><div>+ ${LOCALBASE}/bin/z3:math/z3<br></div><div>+<br></div><div>+USES= gmake bison python shebangfix<br></div><div>+<br></div><div>+USE_GITHUB= yes<br></div><div>+GH_ACCOUNT= diffblue<br></div><div>+SHEBANG_FILES= ${WRKSRC}/scripts/ls_<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://parse.py" target="_blank">parse.py</a><br></div><div>+WRKSRC_minisat= ${WRKDIR}/minisat2-2.2.1<br></div><div>+<br></div><div>+post-patch:<br></div><div>+ @${REINPLACE_CMD} -e 's|.*git describe --tags.*|GIT_INFO = ${PORTNAME}-${PORTVERSION}|' \<br></div><div>+ ${WRKSRC}/src/util/Makefile<br></div><div>+post-extract:<br></div><div>+ @${MV} ${WRKSRC_minisat} ${WRKSRC}/minisat-2.2.1<br></div><div>+<br></div><div>+do-build:<br></div><div>+ @${MKDIR} ${STAGEDIR}<br></div><div>+ cd ${WRKSRC} && ${GMAKE} -C src -j${MAKE_JOBS_NUMBER}<br></div><div>+<br></div><div>+do-install:<br></div><div>+. for x in cbmc crangler goto-analyzer goto-cc goto-diff goto-instrument \<br></div><div>+ goto-inspect goto-harness goto-synthesizer symtab2gb<br></div><div>+ ${INSTALL_PROGRAM} ${WRKSRC}/src/${x}/${x} ${STAGEDIR}${PREFIX}/bin/<br></div><div>+ ${INSTALL_MAN} ${WRKSRC}/doc/man/${x}.1 ${STAGEDIR}${PREFIX}/share/man/man1/<br></div><div>+. endfor<br></div><div>+ ${LN} -sf goto-cc ${STAGEDIR}${PREFIX}/bin/goto-gcc<br></div><div>+ ${LN} -sf goto-cc ${STAGEDIR}${PREFIX}/bin/goto-ld<br></div><div>+ ${INSTALL_SCRIPT} ${WRKSRC}/scripts/ls_<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://parse.py" target="_blank">parse.py</a> ${STAGEDIR}${PREFIX}/bin/<br></div><div>+<br></div><div>+.include <<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://bsd.port.mk>" target="_blank">bsd.port.mk></a>;<br></div><div>diff --git a/devel/cbmc/distinfo b/devel/cbmc/distinfo<br></div><div>new file mode 100644<br></div><div>index 000000000000..f3e6d1161c6a<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/distinfo<br></div><div>@@ -0,0 +1,5 @@<br></div><div>+TIMESTAMP = 1706723199<br></div><div>+SHA256 (minisat2_2.2.1.orig.tar.gz) = e54afa3c192c1753bc8075c0c7e126d5c495d9066e3f90a2588091149ac9ca40<br></div><div>+SIZE (minisat2_2.2.1.orig.tar.gz) = 44229<br></div><div>+SHA256 (diffblue-cbmc-cbmc-5.95.1_GH0.tar.gz) = fdc1e862752430f8d069eb2f9c33dcd05078cf955bbc900e2cc840bcb01b3783<br></div><div>+SIZE (diffblue-cbmc-cbmc-5.95.1_GH0.tar.gz) = 9073428<br></div><div>diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://Solver.cc" target="_blank">Solver.cc</a> b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://Solver.cc" target="_blank">Solver.cc</a><br></div><div>new file mode 100644<br></div><div>index 000000000000..c15c2f12fb0a<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://Solver.cc" target="_blank">Solver.cc</a><br></div><div>@@ -0,0 +1,20 @@<br></div><div>+--- minisat-2.2.1/minisat/core/<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://Solver.cc.orig" target="_blank">Solver.cc.orig</a> 2011-02-21 13:31:17 UTC<br></div><div>++++ minisat-2.2.1/minisat/core/<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://Solver.cc" target="_blank">Solver.cc</a><br></div><div>+@@ -210,7 +210,7 @@ void Solver::cancelUntil(int level) {<br></div><div>+ for (int c = trail.size()-1; c &gt;= trail_lim[level]; c--){<br></div><div>+ Var x = var(trail[c]);<br></div><div>+ assigns [x] = l_Undef;<br></div><div>+- if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())<br></div><div>++ if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last()))<br></div><div>+ polarity[x] = sign(trail[c]);<br></div><div>+ insertVarOrder(x); }<br></div><div>+ qhead = trail_lim[level];<br></div><div>+@@ -666,7 +666,7 @@ lbool Solver::search(int nof_conflicts)<br></div><div>+ <br></div><div>+ }else{<br></div><div>+ // NO CONFLICT<br></div><div>+- if (nof_conflicts &gt;= 0 && conflictC &gt;= nof_conflicts || !withinBudget()){<br></div><div>++ if ((nof_conflicts &gt;= 0 && conflictC &gt;= nof_conflicts) || !withinBudget()){<br></div><div>+ // Reached bound on number of conflicts:<br></div><div>+ progress_estimate = progressEstimate();<br></div><div>+ cancelUntil(0);<br></div><div>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<br></div><div>new file mode 100644<br></div><div>index 000000000000..fa26c6372b36<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_SolverTypes.h<br></div><div>@@ -0,0 +1,59 @@<br></div><div>+--- minisat-2.2.1/minisat/core/SolverTypes.h.orig 2011-02-21 13:31:17 UTC<br></div><div>++++ minisat-2.2.1/minisat/core/SolverTypes.h<br></div><div>+@@ -47,7 +47,7 @@ struct Lit {<br></div><div>+ int x;<br></div><div>+ <br></div><div>+ // Use this as a constructor:<br></div><div>+- friend Lit mkLit(Var var, bool sign = false);<br></div><div>++ //friend Lit mkLit(Var var, bool sign = false);<br></div><div>+ <br></div><div>+ bool operator == (Lit p) const { return x == p.x; }<br></div><div>+ bool operator != (Lit p) const { return x != p.x; }<br></div><div>+@@ -55,7 +55,7 @@ struct Lit {<br></div><div>+ };<br></div><div>+ <br></div><div>+ <br></div><div>+-inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }<br></div><div>++inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; }<br></div><div>+ inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; }<br></div><div>+ inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; }<br></div><div>+ inline bool sign (Lit p) { return p.x & 1; }<br></div><div>+@@ -127,7 +127,10 @@ class Clause {<br></div><div>+ unsigned has_extra : 1;<br></div><div>+ unsigned reloced : 1;<br></div><div>+ unsigned size : 27; } header;<br></div><div>++#include <util/pragma_push.def><br></div><div>++#include <util/pragma_wzero_length_array.def><br></div><div>+ union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];<br></div><div>++#include <util/pragma_pop.def><br></div><div>+ <br></div><div>+ friend class ClauseAllocator;<br></div><div>+ <br></div><div>+@@ -142,11 +145,12 @@ class Clause {<br></div><div>+ for (int i = 0; i < ps.size(); i++) <br></div><div>+ data[i].lit = ps[i];<br></div><div>+ <br></div><div>+- if (header.has_extra)<br></div><div>++ if (header.has_extra) {<br></div><div>+ if (header.learnt)<br></div><div>+ data[header.size].act = 0;<br></div><div>+ else<br></div><div>+ calcAbstraction();<br></div><div>++ }<br></div><div>+ }<br></div><div>+ <br></div><div>+ // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).<br></div><div>+@@ -157,11 +161,12 @@ class Clause {<br></div><div>+ for (int i = 0; i < from.size(); i++)<br></div><div>+ data[i].lit = from[i];<br></div><div>+ <br></div><div>+- if (header.has_extra)<br></div><div>++ if (header.has_extra) {<br></div><div>+ if (header.learnt)<br></div><div>+ data[header.size].act = <a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://from.data[header.size]" target="_blank">from.data[header.size]</a>.act;<br></div><div>+ else <br></div><div>+ data[header.size].abs = <a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://from.data[header.size]" target="_blank">from.data[header.size]</a>.abs;<br></div><div>++ }<br></div><div>+ }<br></div><div>+ <br></div><div>+ public:<br></div><div>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<br></div><div>new file mode 100644<br></div><div>index 000000000000..d8c9ddedb701<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h<br></div><div>@@ -0,0 +1,12 @@<br></div><div>+--- minisat-2.2.1/minisat/mtl/IntTypes.h.orig 2011-02-21 13:31:17 UTC<br></div><div>++++ minisat-2.2.1/minisat/mtl/IntTypes.h<br></div><div>+@@ -31,7 +31,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OT<br></div><div>+ #else<br></div><div>+ <br></div><div>+ # include <stdint.h><br></div><div>++#ifndef _MSC_VER<br></div><div>+ # include <inttypes.h><br></div><div>++#endif<br></div><div>+ <br></div><div>+ #endiffile mode 100644<br></div><div>index 000000000000..f0dd61cd9963<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/files/patch-src_solvers_sat_external__sat.cpp<br></div><div>@@ -0,0 +1,13 @@<br></div><div>+--- src/solvers/sat/external_sat.cpp.orig 2023-10-30 12:11:18 UTC<br></div><div>++++ src/solvers/sat/external_sat.cpp<br></div><div>+@@ -119,8 +119,8 @@ external_satt::resultt external_satt::parse_result(std<br></div><div>+ {<br></div><div>+ try<br></div><div>+ {<br></div><div>+- signed long long as_long = std::stol(assignment_string);<br></div><div>+- size_t index = std::labs(as_long);<br></div><div>++ signed long long as_long = std::stoll(assignment_string);<br></div><div>++ size_t index = std::llabs(as_long);<br></div><div>+ <br></div><div>+ if(index &gt;= number_of_variables)<br></div><div>+ {<br></div><div>diff --git a/devel/cbmc/files/patch-src_util_optional.h b/devel/cbmc/files/patch-src_util_optional.h<br></div><div>new file mode 100644<br></div><div>index 000000000000..4507ce0ade2b<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/files/patch-src_util_optional.h<br></div><div>@@ -0,0 +1,29 @@<br></div><div>+--- src/util/optional.h.orig 2023-10-30 12:11:18 UTC<br></div><div>++++ src/util/optional.h<br></div><div>+@@ -11,20 +11,20 @@ Author: Diffblue Ltd.<br></div><div>+ #define CPROVER_UTIL_OPTIONAL_H<br></div><div>+ <br></div><div>+ #if defined __clang__<br></div><div>+- #pragma clang diagnostic push ignore "-Wall"<br></div><div>+- #pragma clang diagnostic push ignore "-Wpedantic"<br></div><div>++ #pragma clang diagnostic push<br></div><div>++ #pragma clang diagnostic ignored "-Wall"<br></div><div>++ #pragma clang diagnostic ignored "-Wpedantic"<br></div><div>+ #elif defined __GNUC__<br></div><div>+- #pragma GCC diagnostic push ignore "-Wall"<br></div><div>+- #pragma GCC diagnostic push ignore "-Wpedantic"<br></div><div>++ #pragma GCC diagnostic push<br></div><div>++ #pragma GCC diagnostic ignored "-Wall"<br></div><div>++ #pragma GCC diagnostic ignored "-Wpedantic"<br></div><div>+ #elif defined _MSC_VER<br></div><div>+ #pragma warning(push)<br></div><div>+ #endif<br></div><div>+ #include <nonstd/optional.hpp><br></div><div>+ #if defined __clang__<br></div><div>+ #pragma clang diagnostic pop<br></div><div>+- #pragma clang diagnostic pop<br></div><div>+ #elif defined __GNUC__<br></div><div>+- #pragma GCC diagnostic pop<br></div><div>+ #pragma GCC diagnostic pop<br></div><div>+ #elif defined _MSC_VER<br></div><div>+ #pragma warning(pop)<br></div><div>diff --git a/devel/cbmc/pkg-descr b/devel/cbmc/pkg-descr<br></div><div>new file mode 100644<br></div><div>index 000000000000..2004194d7c43<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/pkg-descr<br></div><div>@@ -0,0 +1,7 @@<br></div><div>+CBMC is a Bounded Model Checker for C and C++ programs.<br></div><div>+It supports C89, C99, most of C11 and most compiler extensions provided by gcc<br></div><div>+and Visual Studio. It allows verifying array bounds (buffer overflows), pointer<br></div><div>+safety, exceptions and user-specified assertions. Furthermore, it can check C<br></div><div>+and C++ for consistency with other languages, such as Verilog.<br></div><div>+The verification is performed by unwinding the loops in the program and passing<br></div><div>+the resulting equation to a decision procedure.<br></div><div>diff --git a/devel/cbmc/pkg-plist b/devel/cbmc/pkg-plist<br></div><div>new file mode 100644<br></div><div>index 000000000000..2d23b585ef57<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/pkg-plist<br></div><div>@@ -0,0 +1,23 @@<br></div><div>+bin/cbmc<br></div><div>+bin/crangler<br></div><div>+bin/goto-analyzer<br></div><div>+bin/goto-cc<br></div><div>+bin/goto-diff<br></div><div>+bin/goto-instrument<br></div><div>+bin/goto-inspect<br></div><div>+bin/goto-harness<br></div><div>+bin/goto-synthesizer<br></div><div>+bin/symtab2gb<br></div><div>+bin/ls_<a data-ik="ik-secure" rel="noopener noreferrer" class="defaultMailLink" href="http://parse.py" target="_blank">parse.py</a><br></div><div>+bin/goto-gcc<br></div><div>+bin/goto-ld<br></div><div>+share/man/man1/cbmc.1.gz<br></div><div>+share/man/man1/crangler.1.gz<br></div><div>+share/man/man1/goto-analyzer.1.gz<br></div><div>+share/man/man1/goto-cc.1.gz<br></div><div>+share/man/man1/goto-diff.1.gz<br></div><div>+share/man/man1/goto-harness.1.gz<br></div><div>+share/man/man1/goto-inspect.1.gz<br></div><div>+share/man/man1/goto-instrument.1.gz<br></div><div>+share/man/man1/goto-synthesizer.1.gz<br></div><div>+share/man/man1/symtab2gb.1.gz<br></div></pre></blockquote></div><div>Hi,<br></div><div><br></div><div>Are these patches upstreamed or backported?<br></div><div><br></div><div>Best regards,<br></div><div>Daniel (diizzy@)<br></div><div ><div><br></div></div>home | help
Want to link to this message? Use this
URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?379c7ddb410058469dcda4f67b45caa9>