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 +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 ad8e34a..3af5e64 100644 --- a/cbmc.spec +++ b/cbmc.spec @@ -1,12 +1,11 @@ -%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 -Release: 2%{?dist} +Version: 5.35.0 +Release: 1%{?dist} Summary: Bounded Model Checker for ANSI-C and C++ programs License: BSD with advertising @@ -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/a5b3008411f89a7800fde9003017242a80d84103 # 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_to_include_SSE2) -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 - 5.35.0-1 +- New upstream release +- Use plain doxygen to cut-down some build dependencies + * Wed Jul 21 2021 Fedora Release Engineering - 5.29.0-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild 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