git: 7f087b720e52 - main - devel/cbmc: add new port
- Reply: Daniel Engberg : "Re: git: 7f087b720e52 - main - devel/cbmc: add new port"
- Go to: [ bottom of page ] [ top of archives ] [ this month ]
Date: Thu, 01 Feb 2024 17:55:09 UTC
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 | 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 <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 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 <util/pragma_push.def>
++#include <util/pragma_wzero_length_array.def>
+ union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];
++#include <util/pragma_pop.def>
+
+ friend class ClauseAllocator;
+
+@@ -142,11 +145,12 @@ class Clause {
+ for (int i = 0; i < ps.size(); i++)
+ data[i].lit = ps[i];
+
+- if (header.has_extra)
++ if (header.has_extra) {
+ if (header.learnt)
+ data[header.size].act = 0;
+ else
+ calcAbstraction();
++ }
+ }
+
+ // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
+@@ -157,11 +161,12 @@ class Clause {
+ for (int i = 0; i < from.size(); i++)
+ data[i].lit = from[i];
+
+- if (header.has_extra)
++ if (header.has_extra) {
+ if (header.learnt)
+ data[header.size].act = from.data[header.size].act;
+ else
+ data[header.size].abs = from.data[header.size].abs;
++ }
+ }
+
+ public:
diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h
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
+
+ #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<T>::capacity(int min_cap) {
+ void vec<T>::capacity(int min_cap) {
+ if (cap >= min_cap) return;
+ int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
+- if (add > INT_MAX - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)
++ if (add > INT_MAX - cap)
+ throw OutOfMemoryException();
+- }
++
++ data = (T*)xrealloc(data, (cap += add) * sizeof(T));
++}
+
+
+ template<class T>
diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_XAlloc.h b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_XAlloc.h
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 <errno.h>
+ #include <stdlib.h>
+
+ namespace Minisat {
+@@ -33,7 +32,7 @@ static inline void* xrealloc(void *ptr, size_t size)
+ static inline void* xrealloc(void *ptr, size_t size)
+ {
+ void* mem = realloc(ptr, size);
+- if (mem == NULL && errno == ENOMEM){
++ if (mem == NULL){
+ throw OutOfMemoryException();
+ }else
+ return mem;
diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_simp_SimpSolver.cc b/devel/cbmc/files/patch-minisat-2.2.1_minisat_simp_SimpSolver.cc
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<Lit>& ps)
+ {
+ #ifndef NDEBUG
+@@ -227,10 +225,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause
+ if (var(qs[i]) != v){
+ for (int j = 0; j < ps.size(); j++)
+ if (var(ps[j]) == var(qs[i]))
++ {
+ if (ps[j] == ~qs[i])
+ return false;
+ else
+ goto next;
++ }
+ out_clause.push(qs[i]);
+ }
+ next:;
+@@ -261,10 +261,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause
+ if (var(__qs[i]) != v){
+ for (int j = 0; j < ps.size(); j++)
+ if (var(__ps[j]) == var(__qs[i]))
++ {
+ if (__ps[j] == ~__qs[i])
+ return false;
+ else
+ goto next;
++ }
+ size++;
+ }
+ next:;
diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_Options.cc b/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_Options.cc
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 <stdlib.h>
+ #include <stdio.h>
+
+-#include <zlib.h>
++//#include <zlib.h>
+
+ namespace Minisat {
+
+@@ -35,7 +35,7 @@ class StreamBuffer {
+
+
+ class StreamBuffer {
+- gzFile in;
++ //gzFile in;
+ unsigned char buf[buffer_size];
+ int pos;
+ int size;
+@@ -43,10 +43,10 @@ class StreamBuffer {
+ void assureLookahead() {
+ if (pos >= size) {
+ pos = 0;
+- size = gzread(in, buf, sizeof(buf)); } }
++ /*size = gzread(in, buf, sizeof(buf));*/ } }
+
+ public:
+- explicit StreamBuffer(gzFile i) : in(i), pos(0), size(0) { assureLookahead(); }
++ //explicit StreamBuffer(gzFile i) : in(i), pos(0), size(0) { assureLookahead(); }
+
+ int operator * () const { return (pos >= size) ? EOF : buf[pos]; }
+ void operator ++ () { pos++; assureLookahead(); }
diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_System.h b/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_System.h
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 <fpu_control.h>
+ #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 <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
+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