[cbmc/f20] Updated to 4.6

Fri Dec 6 12:26:00 UTC 2013

commit a02688ccfa42bf8dbdf251d27fc10929dd93a6ad
Author: Shakthi Kannan <skannan at redhat.com>
Date:   Fri Dec 6 17:55:56 2013 +0530

    Updated to 4.6

 .gitignore                             |    1 +
 cbmc-20130515-regression.Makefile      |    4 --
 cbmc-20130515svn-fix-build.patch       |   50 -------------------------
 cbmc-20130515svn-no-long_width.patch   |   26 -------------
 cbmc-20130515svn-regression-test.patch |   64 --------------------------------
 cbmc-20131201svn-fix-build.patch       |   62 +++++++++++++++++++++++++++++++
 cbmc.spec                              |   15 +++----
 sources                                |    2 +-
 8 files changed, 70 insertions(+), 154 deletions(-)
---

diff --git a/.gitignore b/.gitignore
index 110b88a..603cea4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,2 @@
 /cbmc-4.3-20130515svn.tar.gz
+/cbmc-4.6-20131201svn.tar.gz
diff --git a/cbmc-20131201svn-fix-build.patch b/cbmc-20131201svn-fix-build.patch
new file mode 100644
index 0000000..660b03e
--- /dev/null
+++ b/cbmc-20131201svn-fix-build.patch
@@ -0,0 +1,62 @@
+diff -up cbmc-4.6-20131201svn/src/cbmc/Makefile.build cbmc-4.6-20131201svn/src/cbmc/Makefile
+--- cbmc-4.6-20131201svn/src/cbmc/Makefile.build	2013-12-05 16:57:59.848821235 +0530
++++ cbmc-4.6-20131201svn/src/cbmc/Makefile	2013-12-05 16:58:18.806874197 +0530
+@@ -22,7 +22,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
+ 
+ INCLUDES= -I ..
+ 
+-LIBS =
++LIBS = -lminisat
+ 
+ include ../config.inc
+ include ../common
+diff -up cbmc-4.6-20131201svn/src/common.build cbmc-4.6-20131201svn/src/common
+--- cbmc-4.6-20131201svn/src/common.build	2013-12-05 16:58:30.472907110 +0530
++++ cbmc-4.6-20131201svn/src/common	2013-12-05 16:59:08.887018367 +0530
+@@ -23,8 +23,8 @@ ifeq ($(BUILD_ENV_),MinGW)
+ else
+   EXEEXT =
+ endif
+-  CFLAGS ?= -Wall -O2
+-  CXXFLAGS ?= -Wall -O2
++  CFLAGS = ${RPM_OPT_FLAGS} 
++  CXXFLAGS = ${RPM_OPT_FLAGS}
+   CP_CFLAGS = -MMD -MP
+   CP_CXXFLAGS = -MMD -MP -DSTL_HASH_TR1
+   #LINKFLAGS = -static
+diff -up cbmc-4.6-20131201svn/src/config.inc.build cbmc-4.6-20131201svn/src/config.inc
+--- cbmc-4.6-20131201svn/src/config.inc.build	2013-12-05 16:59:23.673062258 +0530
++++ cbmc-4.6-20131201svn/src/config.inc	2013-12-05 16:59:45.511128110 +0530
+@@ -11,7 +11,7 @@ BUILD_ENV = AUTO
+ #CHAFF = ../../zChaff
+ #BOOLEFORCE = ../../booleforce-0.4
+ #MINISAT = ../../MiniSat-p_v1.14
+-MINISAT2 = ../../minisat-2.2.0
++MINISAT2 = /usr/include/minisat 
+ #GLUCOSE = ../../glucose2.2
+ #SMVSAT =
+ 
+diff -up cbmc-4.6-20131201svn/src/goto-instrument/Makefile.build cbmc-4.6-20131201svn/src/goto-instrument/Makefile
+--- cbmc-4.6-20131201svn/src/goto-instrument/Makefile.build	2013-12-05 17:13:11.341134375 +0530
++++ cbmc-4.6-20131201svn/src/goto-instrument/Makefile	2013-12-05 17:13:22.124253011 +0530
+@@ -28,7 +28,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
+ 
+ INCLUDES= -I ..
+ 
+-LIBS =
++LIBS = -lminisat
+ 
+ CLEANFILES = goto-instrument$(EXEEXT)
+ 
+diff -up cbmc-4.6-20131201svn/src/solvers/Makefile.build cbmc-4.6-20131201svn/src/solvers/Makefile
+--- cbmc-4.6-20131201svn/src/solvers/Makefile.build	2013-12-05 16:59:56.553161633 +0530
++++ cbmc-4.6-20131201svn/src/solvers/Makefile	2013-12-05 17:00:05.047187735 +0530
+@@ -17,7 +17,7 @@ endif
+ 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
diff --git a/cbmc.spec b/cbmc.spec
index 9edc548..26e6e1e 100644
--- a/cbmc.spec
+++ b/cbmc.spec
@@ -1,11 +1,11 @@
 # until defined for all current releases
 %{!?_pkgdocdir: %global _pkgdocdir %{_docdir}/%{name}-%{version}}
 
-%global checkout 20130515svn
+%global checkout 20131201svn
 
 Name:           cbmc
-Version:        4.3
-Release:        7.%{checkout}%{?dist}
+Version:        4.6
+Release:        1.%{checkout}%{?dist}
 Summary:        Bounded Model Checker for ANSI-C and C++ programs
 
 License:        BSD with advertising
@@ -16,10 +16,7 @@ URL:            http://www.cprover.org/cbmc/
 #  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
-Source1:        cbmc-20130515-regression.Makefile
 Patch0:         cbmc-%{checkout}-fix-build.patch
-Patch1:         cbmc-%{checkout}-regression-test.patch
-Patch2:         cbmc-%{checkout}-no-long_width.patch
 
 BuildRequires:  flex
 BuildRequires:  bison
@@ -33,10 +30,7 @@ iterations.
 
 %prep
 %setup -q -n %{name}-%{version}-%{checkout}
-cp %{SOURCE1} regression/Makefile
 %patch0 -p1
-%patch1 -p1
-%patch2 -p1
 
 %build
 make %{?_smp_mflags} -C src
@@ -61,6 +55,9 @@ make
 %{_mandir}/man1/cbmc.*
 
 %changelog
+* Sun Dec  1 2013 Shakthi Kannan <shakthimaan [AT] fedoraproject.org> - 4.6-1.20131201svn
+- Updated to upstream 4.6 release
+
 * Tue Sep 10 2013 Shakthi Kannan <shakthimaan [AT] fedoraproject.org> - 4.3-7.20130515svn
 - Fix build with unversioned docdir using _pkgdocdir (#992043)
 
diff --git a/sources b/sources
index 1d9e7ce..eb36ac4 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-f54051a29e1bdc747cc17d359ea34ed5  cbmc-4.3-20130515svn.tar.gz
+02d2dc1e92ef2014459269cd93121a83  cbmc-4.6-20131201svn.tar.gz
