devel/cbmc: add new port

Bounded Model Checker for C and C++ programs
https://github.com/diffblue/cbmc

Sponsored by:	Netflix

18 files changed, 387 insertions, 0 deletions

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