The package rpms/cbmc.git has added or updated architecture specific content in its
spec file (ExclusiveArch/ExcludeArch or %ifarch/%ifnarch) in commit(s):
https://src.fedoraproject.org/cgit/rpms/cbmc.git/commit/?id=85c4b56d1787c....
Change:
+%ifarch %{ix86}
Thanks.
Full change:
============
commit 85c4b56d1787cfaf1cdee2e44b076cb40bd557c6
Author: Vincent Mihalkovic <vmihalko(a)redhat.com>
Date: Thu Aug 5 10:42:52 2021 +0200
New upstream release
diff --git a/cbmc-catch2.patch b/cbmc-catch2.patch
deleted file mode 100644
index d60dbd5..0000000
--- a/cbmc-catch2.patch
+++ /dev/null
@@ -1,13 +0,0 @@
-diff --git unit/catch/catch.hpp unit/catch/catch.hpp
-index 73274e0..0f9a66f 100644
---- unit/catch/catch.hpp
-+++ unit/catch/catch.hpp
-@@ -8166,7 +8166,7 @@ namespace Catch {
-
- // 32kb for the alternate stack seems to be sufficient. However, this value
- // is experimentally determined, so that's not guaranteed.
-- constexpr static std::size_t sigStackSize = 32768 >= MINSIGSTKSZ ? 32768 :
MINSIGSTKSZ;
-+ static constexpr std::size_t sigStackSize = 32768;
-
- static SignalDefs signalDefs[] = {
- { SIGINT, "SIGINT - Terminal interrupt signal" },
diff --git a/cbmc-disable-werror.patch b/cbmc-disable-werror.patch
new file mode 100644
index 0000000..c45f150
--- /dev/null
+++ b/cbmc-disable-werror.patch
@@ -0,0 +1,53 @@
+From 39aa11cb009ab2d838b0f2f223dc002075a29394 Mon Sep 17 00:00:00 2001
+From: Lukas Zaoral <lzaoral(a)redhat.com>
+Date: Wed, 4 Aug 2021 13:15:49 +0200
+Subject: [PATCH] build: do not compile with -Werror
+
+---
+ CMakeLists.txt | 2 +-
+ src/ansi-c/library_check.sh | 2 +-
+ src/config.inc | 2 +-
+ 3 files changed, 3 insertions(+), 3 deletions(-)
+
+diff --git CMakeLists.txt CMakeLists.txt
+index 1cb6c78ec..7667dd453 100644
+--- CMakeLists.txt
++++ CMakeLists.txt
+@@ -62,7 +62,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
+ set(CMAKE_CXX_FLAGS_RELEASE "-O2")
+ set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g")
+ # Enable lots of warnings
+- set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror
-Wno-deprecated-declarations -Wswitch-enum")
++ set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic
-Wno-deprecated-declarations -Wswitch-enum")
+ elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+ # This would be the place to enable warnings for Windows builds, although
+ # config.inc doesn't seem to do that currently
+diff --git a/src/ansi-c/library_check.sh b/src/ansi-c/library_check.sh
+index bb362dc02..bd407ee74 100755
+--- src/ansi-c/library_check.sh
++++ src/ansi-c/library_check.sh
+@@ -11,7 +11,7 @@ for f in "$@"; do
+ perl -p -i -e 's/(__sync_)/s$1/' __libcheck.c
+ perl -p -i -e 's/(__atomic_)/s$1/' __libcheck.c
+ "$CC" -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool
-D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
+- "$CC" -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i \
++ "$CC" -S -Wall -pedantic -Wextra -std=gnu99 __libcheck.i \
+ -o __libcheck.s -Wno-unused-label -Wno-unknown-pragmas
+ ec="${?}"
+ rm __libcheck.s __libcheck.i __libcheck.c
+diff --git src/config.inc src/config.inc
+index 71d5f1d80..bb85390e8 100644
+--- src/config.inc
++++ src/config.inc
+@@ -5,7 +5,7 @@ BUILD_ENV = AUTO
+ ifeq ($(BUILD_ENV),MSVC)
+ #CXXFLAGS += /Wall /WX
+ else
+- CXXFLAGS += -Wall -pedantic -Werror -Wno-deprecated-declarations -Wswitch-enum
++ CXXFLAGS += -Wall -pedantic -Wno-deprecated-declarations -Wswitch-enum
+ endif
+
+ ifeq ($(CPROVER_WITH_PROFILING),1)
+--
+2.31.1
+
diff --git a/cbmc-f35-enable_sse2.patch b/cbmc-f35-enable_sse2.patch
index 6c995ec..1f51f2a 100644
--- a/cbmc-f35-enable_sse2.patch
+++ b/cbmc-f35-enable_sse2.patch
@@ -7,9 +7,9 @@ index bb362dc..3c64fba 100755
perl -p -i -e 's/(__sync_)/s$1/' __libcheck.c
perl -p -i -e 's/(__atomic_)/s$1/' __libcheck.c
- "$CC" -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool
-D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
-- "$CC" -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i \
+- "$CC" -S -Wall -pedantic -Wextra -std=gnu99 __libcheck.i \
+ "$CC" -std=gnu99 -msse2 -E -include library/cprover.h
-D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i
__libcheck.c
-+ "$CC" -S -Wall -Werror -pedantic -Wextra -std=gnu99 -msse2 __libcheck.i \
++ "$CC" -S -Wall -pedantic -Wextra -std=gnu99 -msse2 __libcheck.i \
-o __libcheck.s -Wno-unused-label -Wno-unknown-pragmas
ec="${?}"
rm __libcheck.s __libcheck.i __libcheck.c
diff --git a/cbmc-minisat.patch b/cbmc-minisat.patch
index 9bfe0fa..6f14e20 100644
--- a/cbmc-minisat.patch
+++ b/cbmc-minisat.patch
@@ -12,7 +12,7 @@ index 0d02f80..139ff0a 100644
+
set(sat_impl "minisat2" CACHE STRING
"This setting controls the SAT library which is used. Valid values are
- 'minisat2', 'glucose', or 'cadical'"
+ 'minisat2', 'glucose', 'cadical', 'ipasir-cadical'
or 'ipasir-custom'"
diff --git src/solvers/CMakeLists.txt src/solvers/CMakeLists.txt
index d55ec09..4a6dd4f 100644
--- src/solvers/CMakeLists.txt
diff --git a/cbmc.spec b/cbmc.spec
index d398688..3398558 100644
--- a/cbmc.spec
+++ b/cbmc.spec
@@ -1,11 +1,10 @@
-%undefine __cmake_in_source_build
-
-%define utils_version 1.1
# FIXME: report to upstream
%define _lto_cflags %{nil}
+%define utils_version 1.1
+
Name: cbmc
-Version: 5.29.0
+Version: 5.35.0
Release: 1%{?dist}
Summary: Bounded Model Checker for ANSI-C and C++ programs
@@ -23,25 +22,25 @@ Patch1: %{name}-5.12-fix-f33.patch
Patch2: %{name}-minisat.patch
# Skip some c++ tests as cbmc cannot parse some GCC 11 headers
Patch3: %{name}-f34-fix-build.patch
-# From
https://src.fedoraproject.org/rpms/catch/c/771d2
-Patch4: %{name}-catch2.patch
# Revert
https://github.com/diffblue/cbmc/commit/a5b3008411f89a7800fde9003017242a8...
# due deprecated python2 in fedora
-Patch5: %{name}-f35-deprecated-python.patch
+Patch4: %{name}-f35-deprecated-python.patch
+# Disable -Werror flag
+Patch5: %{name}-disable-werror.patch
# Enable SSE2
(
https://fedoraproject.org/wiki/Changes/Update_i686_architectural_baseline...)
-Patch6: %{name}-f35-enable_sse2.patch
+Patch6: %{name}-f35-enable_sse2.patch
BuildRequires: bison
BuildRequires: cmake
-BuildRequires: doxygen-latex
+BuildRequires: doxygen
BuildRequires: flex
BuildRequires: gcc-c++
BuildRequires: glpk-devel
-BuildRequires: make
BuildRequires: minisat2-devel
BuildRequires: ninja-build
BuildRequires: zlib-devel
-# for the test
+
+# For the tests.
BuildRequires: jq
BuildRequires: gdb
BuildRequires: perl
@@ -66,7 +65,7 @@ Documentation for %{name}.
Summary: Output conversion utilities for CBMC
%description utils
-Output conversion utilities for CBMC (GCC like format)
+Output conversion utilities for CBMC (GCC like format).
%prep
%setup -T -q -b 1 -n %{name}-utils-%{utils_version}
@@ -74,38 +73,31 @@ Output conversion utilities for CBMC (GCC like format)
# FIXME: Upstream the patches
%patch0 -p0
-%if 0%{?fedora} > 32
%patch1 -p0
-%endif
%patch2 -p0
%if 0%{?fedora} > 33
%patch3 -p0
%endif
%patch4 -p0
%patch5 -p0
-%ifarch i686
+%ifarch %{ix86}
%patch6 -p0
%endif
%build
-%cmake -GNinja -DWITH_JBMC:BOOL=OFF -DWITH_SYSTEM_SAT_SOLVER:BOOL=ON
-DBUILD_SHARED_LIBS:BOOL=OFF
+%cmake -GNinja -DWITH_JBMC:BOOL=OFF \
+ -DWITH_SYSTEM_SAT_SOLVER:BOOL=ON \
+ -DBUILD_SHARED_LIBS:BOOL=OFF
%cmake_build
-
-# Build the documentation, TODO: build the doc with cmake
-make -C src doc
+%cmake_build --target doc
%install
%cmake_install
-# Remove useless manpages
-rm %{buildroot}%{_mandir}/man1/j{bmc,analyzer,diff}.1
-
install -p -m 0755
"%{_builddir}/%{name}-utils-%{utils_version}/cbmc_utils/formatCBMCOutput.py"
%{buildroot}%{_bindir}/%{name}-convert-output
install -p -m 0755
"%{_builddir}/%{name}-utils-%{utils_version}/cbmc_utils/csexec-cbmc.sh"
%{buildroot}%{_bindir}/csexec-%{name}
-# goto-clang is (by default) generating hybrid binary
-ln -s %{_bindir}/goto-cc %{buildroot}%{_bindir}/goto-clang
-
+# FIXME: What is this.
# Feed the debuginfo generator
ln -s xml_y.tab.h src/xmllang/xml_y.tab.hpp
@@ -124,7 +116,7 @@ ln -s xml_y.tab.h src/xmllang/xml_y.tab.hpp
%{_mandir}/man1/*
%files doc
-%doc doc/html
+%doc %{__cmake_builddir}/doc/html
%license LICENSE
%files utils
@@ -132,8 +124,11 @@ ln -s xml_y.tab.h src/xmllang/xml_y.tab.hpp
%{_bindir}/%{name}-convert-output
%{_bindir}/csexec-%{name}
-
%changelog
+* Wed Aug 4 2021 Lukas Zaoral <lzaoral(a)redhat.com> - 5.35.0-1
+- New upstream release
+- Use plain doxygen to cut-down some build dependencies
+
* Wed May 12 2021 Vincent Mihalkovic <vmihalko(a)redhat.com> - 5.29.0-1
- New upstream release
diff --git a/sources b/sources
index 86311bc..a470fb8 100644
--- a/sources
+++ b/sources
@@ -1,2 +1,2 @@
-SHA512 (cbmc-5.29.0.tar.gz) =
23402f72f13a04096d7a3cea8e570620558288118231833bf8cd4f3f47c85f11ed2719f5330f570b9263a5732999800017ec910dfe84b96dbd0326ad77ecf2c3
+SHA512 (cbmc-5.35.0.tar.gz) =
bbd6470989dcdcef6090301b4c0ffc32339993824ac25e2b87cba24ace330a4cf8454350456d40d21b1b5b5e52ff05cf7809871ebc9e165edb46c0abe8ec94a1
SHA512 (cbmc-utils-1.1.tar.gz) =
d6170e08cc8b8c6a116cc5db883f8d13dfa976087434468eae1e213c8aada3ebf1bf913e565ff971defbe06106ad4180a5cff1a32bbbb2ee3b035a7600b0183c