Re: git: 7f087b720e52 - main - devel/cbmc: add new port
Date: Fri, 02 Feb 2024 00:05:00 UTC
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@)