[cbmc] Updated to 4.6
Shakthi Kannan
shakthimaan at fedoraproject.org
Fri Dec 6 12:19:20 UTC 2013
commit 9c10ba9710707aec02a1a9fc24aee4c27910505f
Author: Shakthi Kannan <skannan at redhat.com>
Date: Fri Dec 6 17:49:12 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
More information about the scm-commits
mailing list