[cbmc] New upstream release. Build with CUDD support.
Jerry James
jjames at fedoraproject.org
Wed Jun 25 22:30:31 UTC 2014
commit b587833e40920a4f2943d0a78a9f0d3cadeb24f1
Author: Jerry James <jamesjer at betterlinux.com>
Date: Wed Jun 25 16:18:34 2014 -0600
New upstream release.
Build with CUDD support.
.gitignore | 3 +-
cbmc-20131201svn-fix-build.patch | 62 -------------------------
cbmc-4.7-alias.patch | 40 ++++++++++++++++
cbmc-4.7-cudd.patch | 28 +++++++++++
cbmc-4.7-fix-build.patch | 93 ++++++++++++++++++++++++++++++++++++++
cbmc.spec | 66 +++++++++++++++++----------
sources | 2 +-
7 files changed, 205 insertions(+), 89 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index 603cea4..33dc8d0 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1 @@
-/cbmc-4.3-20130515svn.tar.gz
-/cbmc-4.6-20131201svn.tar.gz
+/cbmc-4.7.tar.xz
diff --git a/cbmc-4.7-alias.patch b/cbmc-4.7-alias.patch
new file mode 100644
index 0000000..86c1862
--- /dev/null
+++ b/cbmc-4.7-alias.patch
@@ -0,0 +1,40 @@
+Index: src/cpp/cpp_typecheck_constructor.cpp
+===================================================================
+--- src/cpp/cpp_typecheck_constructor.cpp (revision 4158)
++++ src/cpp/cpp_typecheck_constructor.cpp (working copy)
+@@ -333,7 +333,7 @@
+ codet mem_init("member_initializer");
+ mem_init.location() = location;
+ mem_init.set(ID_member, cppname);
+- mem_init.copy_to_operands((const exprt&)cpparg);
++ mem_init.copy_to_operands(cpparg);
+ initializers.move_to_sub(mem_init);
+ }
+ }
+@@ -396,7 +396,7 @@
+
+ exprt memberexpr(ID_member);
+ memberexpr.set("component_cpp_name",cppname);
+- memberexpr.copy_to_operands((const exprt&)cpparg);
++ memberexpr.copy_to_operands(cpparg);
+ memberexpr.location() = location;
+
+ if(mem_it->type().id()==ID_array)
+Index: src/util/expr.h
+===================================================================
+--- src/util/expr.h (revision 4158)
++++ src/util/expr.h (working copy)
+@@ -111,6 +111,13 @@
+ void copy_to_operands(const exprt &e1, const exprt &e2); // does not destroy expr
+ void copy_to_operands(const exprt &e1, const exprt &e2, const exprt &e3); // does not destroy expr
+
++ inline void copy_to_operands(const irept &irep)
++ #ifdef OPERANDS_IN_GETSUB
++ { return get_sub().push_back(irep); }
++ #else
++ { return add(ID_operands).get_sub().push_back(irep); }
++ #endif
++
+ // the following are deprecated -- use constructors instead
+ void make_typecast(const typet &_type);
+ void make_not();
diff --git a/cbmc-4.7-cudd.patch b/cbmc-4.7-cudd.patch
new file mode 100644
index 0000000..52fb347
--- /dev/null
+++ b/cbmc-4.7-cudd.patch
@@ -0,0 +1,28 @@
+Index: src/solvers/qbf/qbf_bdd_core.cpp
+===================================================================
+--- src/solvers/qbf/qbf_bdd_core.cpp (revision 4158)
++++ src/solvers/qbf/qbf_bdd_core.cpp (working copy)
+@@ -8,6 +8,7 @@
+
+ #include <cassert>
+ #include <fstream>
++#include <iostream>
+
+ #include <util/i2string.h>
+ #include <util/arith_tools.h>
+Index: src/solvers/qbf/qbf_skizzo_core.cpp
+===================================================================
+--- src/solvers/qbf/qbf_skizzo_core.cpp (revision 4158)
++++ src/solvers/qbf/qbf_skizzo_core.cpp (working copy)
+@@ -358,9 +358,9 @@
+ DdNode *negNode = bdds[2*i+1];
+
+ if(Cudd_DagSize(posNode) <= Cudd_DagSize(negNode))
+- model_bdds[cur]=new BDD(bdd_manager, posNode);
++ model_bdds[cur]=new BDD(*bdd_manager, posNode);
+ else
+- model_bdds[cur]=new BDD(bdd_manager, Cudd_Not(negNode));
++ model_bdds[cur]=new BDD(*bdd_manager, Cudd_Not(negNode));
+ }
+
+ // tell CUDD that we don't need those BDDs anymore.
diff --git a/cbmc-4.7-fix-build.patch b/cbmc-4.7-fix-build.patch
new file mode 100644
index 0000000..44a8dc8
--- /dev/null
+++ b/cbmc-4.7-fix-build.patch
@@ -0,0 +1,93 @@
+Index: src/cbmc/Makefile
+===================================================================
+--- src/cbmc/Makefile (revision 4158)
++++ src/cbmc/Makefile (working copy)
+@@ -23,7 +23,7 @@
+
+ INCLUDES= -I ..
+
+-LIBS =
++LIBS = -lminisat -lcuddobj -lcudd -lmtr -lcuddst -lcuddutil -lepd -ldddmp
+
+ include ../config.inc
+ include ../common
+Index: src/common
+===================================================================
+--- src/common (revision 4158)
++++ src/common (working copy)
+@@ -45,7 +45,7 @@
+ else
+ LINKLIB = ld -r -o $@ $^
+ endif
+- LINKBIN = $(CXX) $(LINKFLAGS) -o $@ $^ $(LIBS)
++ LINKBIN = $(CXX) $(LINKFLAGS) -o $@ $^ $(LDFLAGS) $(LIBS)
+ LINKNATIVE = $(HOSTCXX) -o $@ $^
+ ifeq ($(origin CC),default)
+ CC = gcc
+Index: src/config.inc
+===================================================================
+--- src/config.inc (revision 4158)
++++ src/config.inc (working copy)
+@@ -2,16 +2,19 @@
+ BUILD_ENV = AUTO
+
+ # Variables you may want to override
+-#CXXFLAGS = -Wall -O0 -g -Werror -Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing -pedantic
++CFLAGS = @RPM_OPT_FLAGS@
++CXXFLAGS = @RPM_OPT_FLAGS@
++LDFLAGS = @RPM_LD_FLAGS@
+
+ # SAT-solvers we have
+ #PRECOSAT = ../../precosat-576-7e5e66f-120112
+ #PICOSAT = ../../picosat-936
++CUDD = /usr
+ #LINGELING = ../../lingeling-587f-4882048-110513
+ #CHAFF = ../../zChaff
+ #BOOLEFORCE = ../../booleforce-0.4
+ #MINISAT = ../../MiniSat-p_v1.14
+-MINISAT2 = ../../minisat-2.2.0
++MINISAT2 = /usr/include/minisat
+ #GLUCOSE = ../../glucose2.2
+ #SMVSAT =
+
+Index: src/goto-instrument/Makefile
+===================================================================
+--- src/goto-instrument/Makefile (revision 4158)
++++ src/goto-instrument/Makefile (working copy)
+@@ -28,7 +28,7 @@
+
+ INCLUDES= -I ..
+
+-LIBS =
++LIBS = -lminisat -lcuddobj -lcudd -lmtr -lcuddst -lcuddutil -lepd -ldddmp
+
+ CLEANFILES = goto-instrument$(EXEEXT)
+
+Index: src/solvers/Makefile
+===================================================================
+--- src/solvers/Makefile (revision 4158)
++++ src/solvers/Makefile (working copy)
+@@ -17,7 +17,7 @@
+ ifneq ($(MINISAT2),)
+ MINISAT2_SRC=sat/satcheck_minisat2.cpp
+ MINISAT2_INCLUDE=-I $(MINISAT2)
+- MINISAT2_LIB=$(MINISAT2)/simp/SimpSolver$(OBJEXT) $(MINISAT2)/core/Solver$(OBJEXT)
++# MINISAT2_LIB=$(MINISAT2)/simp/SimpSolver$(OBJEXT) $(MINISAT2)/core/Solver$(OBJEXT)
+ CP_CXXFLAGS += -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
+ override CXXFLAGS := $(filter-out -pedantic, $(CXXFLAGS))
+ endif
+@@ -44,10 +44,10 @@
+
+ ifneq ($(CUDD),)
+ CUDD_SRC=qbf/qbf_bdd_core.cpp qbf/qbf_skizzo_core.cpp
+- CUDD_INCLUDE=-I $(CUDD)/include
+- CUDD_LIB=-L $(CUDD)/cudd -L $(CUDD)/util -L $(CUDD)/mtr \
+- -L $(CUDD)/st -L $(CUDD)/obj -L $(CUDD)/dddmp \
+- -L $(CUDD)/epd -lobj -lcudd -lmtr -lst -lutil -lepd -ldddmp
++ CUDD_INCLUDE=-I $(CUDD)/include/cudd
++# CUDD_LIB=-L $(CUDD)/cudd -L $(CUDD)/util -L $(CUDD)/mtr \
++# -L $(CUDD)/st -L $(CUDD)/obj -L $(CUDD)/dddmp \
++# -L $(CUDD)/epd -lobj -lcudd -lmtr -lst -lutil -lepd -ldddmp
+ endif
+
+ ifneq ($(PRECOSAT),)
diff --git a/cbmc.spec b/cbmc.spec
index c1e9e97..e61db44 100644
--- a/cbmc.spec
+++ b/cbmc.spec
@@ -1,27 +1,29 @@
-# until defined for all current releases
-%{!?_pkgdocdir: %global _pkgdocdir %{_docdir}/%{name}-%{version}}
-
-%global checkout 20131201svn
-
Name: cbmc
-Version: 4.6
-Release: 2.%{checkout}%{?dist}
+Version: 4.7
+Release: 1%{?dist}
Summary: Bounded Model Checker for ANSI-C and C++ programs
License: BSD with advertising
URL: http://www.cprover.org/cbmc/
-# The source for this package was pulled from upstream's vcs. Use the
-# following commands to generate the tarball:
-# svn export -r 2441 http://www.cprover.org/svn/cbmc/releases/cbmc-4.3 cbmc-4.3-20130515svn
-# tar czvf cbmc-4.3-20130515svn.tar.gz cbmc-4.3-20130515svn
-Source0: cbmc-%{version}-%{checkout}.tar.gz
-Patch0: cbmc-%{checkout}-fix-build.patch
+# Upstream does not provide tarballs, but rather subversion release branches.
+# Use the following commands to generate the tarball:
+# svn export http://www.cprover.org/svn/cbmc/releases/cbmc-%%{version}
+# tar cJvf cbmc-%%{version}.tar.xz cbmc-%%{version}
+Source0: %{name}-%{version}.tar.xz
+# Fedora-specific patch: set up our build options
+Patch0: %{name}-4.7-fix-build.patch
+# Fix breaking of strict aliasing rules. Sent upstream 25 Jun 2014.
+Patch1: %{name}-4.7-alias.patch
+# Fix the CUDD interface build. Sent upstream 25 Jun 2014.
+Patch2: %{name}-4.7-cudd.patch
-BuildRequires: flex
BuildRequires: bison
-BuildRequires: zlib-devel
+BuildRequires: cudd-devel
+BuildRequires: flex
BuildRequires: minisat2-devel
+BuildRequires: tex(latex)
+BuildRequires: zlib-devel
%description
CBMC generates traces that demonstrate how an assertion can be violated, or
@@ -29,32 +31,48 @@ proves that the assertion cannot be violated within a given number of loop
iterations.
%prep
-%setup -q -n %{name}-%{version}-%{checkout}
-%patch0 -p1
+%setup -q
+%patch0
+%patch1
+%patch2
+
+# Use the right build flags
+sed -e "s|@RPM_OPT_FLAGS@|$RPM_OPT_FLAGS|" \
+ -e "s|@RPM_LD_FLAGS@|-Wl,--as-needed $RPM_LD_FLAGS|" \
+ -i src/config.inc
%build
make %{?_smp_mflags} -C src
+# Build the guide
+pushd doc/guide
+pdflatex CBMC-guide.tex
+pdflatex CBMC-guide.tex
+popd
+
%install
-mkdir -p %{buildroot}%{_bindir} %{buildroot}%{_pkgdocdir}/%{name}-%{version} %{buildroot}%{_mandir}/man1
-install -p src/cbmc/cbmc %{buildroot}%{_bindir}
-install -p src/goto-cc/goto-cc %{buildroot}%{_bindir}
-install -p src/goto-instrument/goto-instrument %{buildroot}%{_bindir}
-cp -pr doc/html-manual %{buildroot}%{_pkgdocdir}/%{name}-%{version}
-install -p doc/man/cbmc.1 %{buildroot}%{_mandir}/man1
+mkdir -p %{buildroot}%{_bindir} %{buildroot}%{_mandir}/man1
+install -p -m 0755 src/cbmc/cbmc %{buildroot}%{_bindir}
+install -p -m 0755 src/goto-cc/goto-cc %{buildroot}%{_bindir}
+install -p -m 0755 src/goto-instrument/goto-instrument %{buildroot}%{_bindir}
+install -p -m 0644 doc/man/cbmc.1 %{buildroot}%{_mandir}/man1
%check
cd regression
make
%files
-%doc CHANGELOG CODING_STANDARD LICENSE
+%doc CHANGELOG LICENSE doc/guide/CBMC-guide.pdf doc/html-manual
%{_bindir}/cbmc
%{_bindir}/goto-cc
%{_bindir}/goto-instrument
%{_mandir}/man1/cbmc.*
%changelog
+* Wed Jun 25 2014 Jerry James <loganjerry at gmail.com> - 4.7-1
+- New upstream release
+- Build with CUDD support
+
* Sat Jun 07 2014 Fedora Release Engineering <rel-eng at lists.fedoraproject.org> - 4.6-2.20131201svn
- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild
diff --git a/sources b/sources
index eb36ac4..1926101 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-02d2dc1e92ef2014459269cd93121a83 cbmc-4.6-20131201svn.tar.gz
+ef596226d5c29457db2e219af2d7aeda cbmc-4.7.tar.xz
More information about the scm-commits
mailing list