[cbmc] First commit
Shakthi Kannan
shakthimaan at fedoraproject.org
Mon Jul 8 15:26:54 UTC 2013
commit b27b4df25f230105bc85e11451603a496e8890e7
Author: Shakthi Kannan <skannan at redhat.com>
Date: Mon Jul 8 20:56:40 2013 +0530
First commit
.gitignore | 1 +
cbmc-20130515-regression.Makefile | 4 ++
cbmc-20130515svn-fix-build.patch | 50 +++++++++++++++++++++++
cbmc-20130515svn-regression-test.patch | 64 +++++++++++++++++++++++++++++
cbmc.spec | 70 ++++++++++++++++++++++++++++++++
sources | 1 +
6 files changed, 190 insertions(+), 0 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index e69de29..110b88a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -0,0 +1 @@
+/cbmc-4.3-20130515svn.tar.gz
diff --git a/cbmc-20130515-regression.Makefile b/cbmc-20130515-regression.Makefile
new file mode 100644
index 0000000..f64e706
--- /dev/null
+++ b/cbmc-20130515-regression.Makefile
@@ -0,0 +1,4 @@
+DIRS = ansi-c cbmc cpp
+
+test:
+ $(foreach var,$(DIRS), make -C $(var) test;)
diff --git a/cbmc-20130515svn-fix-build.patch b/cbmc-20130515svn-fix-build.patch
new file mode 100644
index 0000000..a586648
--- /dev/null
+++ b/cbmc-20130515svn-fix-build.patch
@@ -0,0 +1,50 @@
+diff -up cbmc-20130515/src/cbmc/Makefile.build cbmc-20130515/src/cbmc/Makefile
+--- cbmc-20130515/src/cbmc/Makefile.build 2013-05-15 12:50:59.520072224 +0530
++++ cbmc-20130515/src/cbmc/Makefile 2013-05-15 12:52:15.134092364 +0530
+@@ -21,7 +21,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
+
+ INCLUDES= -I .. -I ../util
+
+-LIBS =
++LIBS = -lminisat
+
+ include ../config.inc
+ include ../common
+diff -up cbmc-20130515/src/common.build cbmc-20130515/src/common
+--- cbmc-20130515/src/common.build 2013-05-15 14:40:37.091528134 +0530
++++ cbmc-20130515/src/common 2013-05-15 14:41:10.354534882 +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-20130515/src/config.inc.build cbmc-20130515/src/config.inc
+--- cbmc-20130515/src/config.inc.build 2013-05-15 12:48:54.624044465 +0530
++++ cbmc-20130515/src/config.inc 2013-05-15 12:50:36.670067670 +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
+ #SMVSAT =
+
+ # Signing identity for MacOS Gatekeeper
+diff -up cbmc-20130515/src/solvers/Makefile.build cbmc-20130515/src/solvers/Makefile
+--- cbmc-20130515/src/solvers/Makefile.build 2013-05-15 12:52:25.056094473 +0530
++++ cbmc-20130515/src/solvers/Makefile 2013-05-15 12:52:35.070096531 +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-20130515svn-regression-test.patch b/cbmc-20130515svn-regression-test.patch
new file mode 100644
index 0000000..48d1293
--- /dev/null
+++ b/cbmc-20130515svn-regression-test.patch
@@ -0,0 +1,64 @@
+diff -up cbmc-20130515/regression/ansi-c/Makefile.test cbmc-20130515/regression/ansi-c/Makefile
+--- cbmc-20130515/regression/ansi-c/Makefile.test 2013-05-15 16:35:47.352904536 +0530
++++ cbmc-20130515/regression/ansi-c/Makefile 2013-05-15 16:36:15.766911601 +0530
+@@ -1,10 +1,10 @@
+ default: tests.log
+
+ test:
+- @../test.pl -c goto-cc
++ @../test.pl -c ../../../src/goto-cc/goto-cc
+
+ tests.log: ../test.pl
+- @../test.pl -c goto-cc
++ @../test.pl -c ../../../src/goto-cc/goto-cc
+
+ show:
+ @for dir in *; do \
+diff -up cbmc-20130515/regression/cbmc-cpp/Makefile.test cbmc-20130515/regression/cbmc-cpp/Makefile
+--- cbmc-20130515/regression/cbmc-cpp/Makefile.test 2013-05-15 16:36:59.128922209 +0530
++++ cbmc-20130515/regression/cbmc-cpp/Makefile 2013-05-15 16:37:37.511931079 +0530
+@@ -1,10 +1,10 @@
+ default: tests.log
+
+ test:
+- @../test.pl -c cbmc
++ @../test.pl -c ../../../src/cbmc/cbmc
+
+ tests.log: ../test.pl
+- @../test.pl -c cbmc
++ @../test.pl -c ../../../src/cbmc/cbmc
+
+ show:
+ @for dir in *; do \
+diff -up cbmc-20130515/regression/cbmc/Makefile.test cbmc-20130515/regression/cbmc/Makefile
+--- cbmc-20130515/regression/cbmc/Makefile.test 2013-05-15 16:36:25.768914162 +0530
++++ cbmc-20130515/regression/cbmc/Makefile 2013-05-15 16:36:44.998918882 +0530
+@@ -1,10 +1,10 @@
+ default: tests.log
+
+ test:
+- @../test.pl -c cbmc
++ @../test.pl -c ../../../src/cbmc/cbmc
+
+ tests.log: ../test.pl
+- @../test.pl -c cbmc
++ @../test.pl -c ../../../src/cbmc/cbmc
+
+ show:
+ @for dir in *; do \
+diff -up cbmc-20130515/regression/cpp/Makefile.test cbmc-20130515/regression/cpp/Makefile
+--- cbmc-20130515/regression/cpp/Makefile.test 2013-05-15 16:37:58.632936075 +0530
++++ cbmc-20130515/regression/cpp/Makefile 2013-05-15 16:38:19.591941154 +0530
+@@ -1,10 +1,10 @@
+ default: tests.log
+
+ test:
+- @../test.pl -c goto-cc
++ @../test.pl -c ../../../src/goto-cc/goto-cc
+
+ tests.log: ../test.pl
+- @../test.pl -c goto-cc
++ @../test.pl -c ../../../src/goto-cc/goto-cc
+
+ show:
+ @for dir in *; do \
diff --git a/cbmc.spec b/cbmc.spec
new file mode 100644
index 0000000..53b0f4b
--- /dev/null
+++ b/cbmc.spec
@@ -0,0 +1,70 @@
+%global checkout 20130515svn
+
+Name: cbmc
+Version: 4.3
+Release: 4.%{checkout}%{?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
+Source1: cbmc-20130515-regression.Makefile
+Patch0: cbmc-%{checkout}-fix-build.patch
+Patch1: cbmc-%{checkout}-regression-test.patch
+
+BuildRequires: flex
+BuildRequires: bison
+BuildRequires: zlib-devel
+BuildRequires: minisat2-devel
+
+%description
+CBMC generates traces that demonstrate how an assertion can be violated, or
+proves that the assertion cannot be violated within a given number of loop
+iterations.
+
+%prep
+%setup -q -n %{name}-%{version}-%{checkout}
+cp %{SOURCE1} regression/Makefile
+%patch0 -p1
+%patch1 -p1
+
+%build
+make %{?_smp_mflags} -C src
+
+%install
+mkdir -p %{buildroot}%{_bindir} %{buildroot}%{_docdir}/%{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}%{_docdir}/%{name}-%{version}
+install -p doc/man/cbmc.1 %{buildroot}%{_mandir}/man1
+
+%check
+cd regression
+make
+
+%files
+%doc CHANGELOG CODING_STANDARD LICENSE
+%{_bindir}/cbmc
+%{_bindir}/goto-cc
+%{_bindir}/goto-instrument
+%{_mandir}/man1/cbmc.*
+
+%changelog
+* Mon Jul 8 2013 Shakthi Kannan <shakthimaan [AT] fedoraproject.org> - 4.3-4.20130515svn
+- Fixed changelog date
+
+* Sun Jun 30 2013 Shakthi Kannan <shakthimaan [AT] fedoraproject.org> - 4.3-3.20130515svn
+- Updated license
+- Fixed doc and manual page directories
+
+* Tue Jun 25 2013 Shakthi Kannan <shakthimaan [AT] fedoraproject.org> - 4.3-2.20130515svn
+- Updated release
+
+* Wed May 15 2013 Shakthi Kannan <shakthimaan [AT] fedoraproject.org> - 4.3-1.20130515svn
+- First release
diff --git a/sources b/sources
index e69de29..1d9e7ce 100644
--- a/sources
+++ b/sources
@@ -0,0 +1 @@
+f54051a29e1bdc747cc17d359ea34ed5 cbmc-4.3-20130515svn.tar.gz
More information about the scm-commits
mailing list