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=32fc2fbb50703....
Change:
+%ifarch armv7hl i686
Thanks.
Full change:
============
commit 32fc2fbb50703d31f9bfc0f2dd0f20648aeb0832
Author: Vincent Mihalkovic <vmihalko(a)redhat.com>
Date: Mon Mar 8 17:20:05 2021 +0100
New upstream release
diff --git a/cbmc-5.12-fix-f33.patch b/cbmc-5.12-fix-f33.patch
index 21fb5d5..14f148c 100644
--- a/cbmc-5.12-fix-f33.patch
+++ b/cbmc-5.12-fix-f33.patch
@@ -3,7 +3,7 @@ index a003b07..2068caa 100644
--- regression/cpp/virtual1/test.desc
+++ regression/cpp/virtual1/test.desc
@@ -1,4 +1,4 @@
--CORE
+-CORE macos-assert-broken
+KNOWNBUG fedora-problem
main.cpp
diff --git a/cbmc-catch2.patch b/cbmc-catch2.patch
new file mode 100644
index 0000000..d60dbd5
--- /dev/null
+++ b/cbmc-catch2.patch
@@ -0,0 +1,13 @@
+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-errno-realpath.patch b/cbmc-errno-realpath.patch
new file mode 100644
index 0000000..0283f9d
--- /dev/null
+++ b/cbmc-errno-realpath.patch
@@ -0,0 +1,14 @@
+diff --git src/util/tempdir.cpp src/util/tempdir.cpp
+index d61636b..c1fb7a9 100644
+--- src/util/tempdir.cpp
++++ src/util/tempdir.cpp
+@@ -93,7 +93,8 @@ std::string get_temporary_directory(const std::string
&name_template)
+ errno = 0;
+ char *wd = realpath(td, nullptr);
+
+- if(wd == nullptr || errno != 0)
++ // Comment out due to the errno realpath problem
++ if(wd == nullptr /* || errno != 0 */)
+ throw system_exceptiont(
+ std::string("realpath failed: ") + std::strerror(errno));
+
diff --git a/cbmc-f34-fix-build.patch b/cbmc-f34-fix-build.patch
new file mode 100644
index 0000000..a363d05
--- /dev/null
+++ b/cbmc-f34-fix-build.patch
@@ -0,0 +1,70 @@
+diff --git regression/ansi-c/array_initialization1/test.desc
regression/ansi-c/array_initialization1/test.desc
+index 466da18..4f89b21 100644
+--- regression/ansi-c/array_initialization1/test.desc
++++ regression/ansi-c/array_initialization1/test.desc
+@@ -1,4 +1,4 @@
+-CORE
++KNOWNBUG rawhide-problem-gcc11-cbmc-compatibility
+ main.c
+
+ ^EXIT=0$
+diff --git regression/ansi-c/float_constant2/test.desc
regression/ansi-c/float_constant2/test.desc
+index dbb23d0..4f89b21 100644
+--- regression/ansi-c/float_constant2/test.desc
++++ regression/ansi-c/float_constant2/test.desc
+@@ -1,4 +1,4 @@
+-CORE test-c++-front-end macos-assert-broken
++KNOWNBUG rawhide-problem-gcc11-cbmc-compatibility
+ main.c
+
+ ^EXIT=0$
+diff --git regression/ansi-c/goto_convert_switch_range_case_valid/test.desc
regression/ansi-c/goto_convert_switch_range_case_valid/test.desc
+index 6f2f5c6..53f62d2 100644
+--- regression/ansi-c/goto_convert_switch_range_case_valid/test.desc
++++ regression/ansi-c/goto_convert_switch_range_case_valid/test.desc
+@@ -1,4 +1,4 @@
+-CORE test-c++-front-end macos-assert-broken
++KNOWNBUG rawhide-problem-gcc11-cbmc-compatibility
+ main.c
+
+ ^EXIT=0$
+diff --git regression/cpp/Method_qualifier1/test.desc
regression/cpp/Method_qualifier1/test.desc
+index 81dc5b6..a92a481 100644
+--- regression/cpp/Method_qualifier1/test.desc
++++ regression/cpp/Method_qualifier1/test.desc
+@@ -1,4 +1,4 @@
+-CORE winbug macos-assert-broken
++KNOWNBUG rawhide-problem-gcc11-cbmc-compatibility
+ main.cpp
+
+ ^EXIT=0$
+diff --git regression/cpp/enum5/test.desc regression/cpp/enum5/test.desc
+index c6e03fd..c2e77d6 100644
+--- regression/cpp/enum5/test.desc
++++ regression/cpp/enum5/test.desc
+@@ -1,4 +1,4 @@
+-CORE winbug macos-assert-broken
++KNOWNBUG rawhide-problem-gcc11-cbmc-compatibility
+ main.cpp
+
+ ^EXIT=0$
+diff --git regression/cpp/switch1/test.desc regression/cpp/switch1/test.desc
+index c6e03fd..c2e77d6 100644
+--- regression/cpp/switch1/test.desc
++++ regression/cpp/switch1/test.desc
+@@ -1,4 +1,4 @@
+-CORE winbug macos-assert-broken
++KNOWNBUG rawhide-problem-gcc11-cbmc-compatibility
+ main.cpp
+
+ ^EXIT=0$
+diff --git regression/ansi-c/array_initialization2/test.desc
regression/ansi-c/array_initialization2/test.desc
+index dbb23d0..4f89b21 100644
+--- regression/ansi-c/array_initialization2/test.desc
++++ regression/ansi-c/array_initialization2/test.desc
+@@ -1,4 +1,4 @@
+-CORE test-c++-front-end macos-assert-broken
++KNOWNBUG rawhide-problem-gcc11-cbmc-compatibility
+ main.c
+
+ ^EXIT=0$
diff --git a/cbmc-goto-cc-type-change.patch b/cbmc-goto-cc-type-change.patch
new file mode 100644
index 0000000..abd3bb8
--- /dev/null
+++ b/cbmc-goto-cc-type-change.patch
@@ -0,0 +1,13 @@
+diff --git src/goto-cc/ms_link_cmdline.cpp src/goto-cc/ms_link_cmdline.cpp
+index 771b45c..e0a8a06 100644
+--- src/goto-cc/ms_link_cmdline.cpp
++++ src/goto-cc/ms_link_cmdline.cpp
+@@ -333,7 +333,7 @@ void ms_link_cmdlinet::process_link_option(const std::string &s)
+ return;
+ }
+
+- for(const std::string &ms_link_option : ms_link_options)
++ for(const std::string ms_link_option : ms_link_options)
+ {
+ // These are case insensitive.
+ if(
diff --git a/cbmc-minisat.patch b/cbmc-minisat.patch
index 9b1bdd1..9bfe0fa 100644
--- a/cbmc-minisat.patch
+++ b/cbmc-minisat.patch
@@ -1,31 +1,31 @@
diff --git CMakeLists.txt CMakeLists.txt
-index 21fb43623..d3e113a70 100644
+index 0d02f80..139ff0a 100644
--- CMakeLists.txt
+++ CMakeLists.txt
-@@ -57,6 +57,10 @@ endif()
+@@ -79,6 +79,10 @@ endif()
set(enable_cbmc_tests on CACHE BOOL "Whether CBMC tests should be enabled")
+option(WITH_SYSTEM_SAT_SOLVER OFF
-+ "This setting controls the SAT library which is used. If option is set system SAT
library
-+ is used")
++ "This setting controls the SAT library which is used. If option is set system SAT
library
++ is used")
+
set(sat_impl "minisat2" CACHE STRING
- "This setting controls the SAT library which is used. Valid values are
'minisat2' and 'glucose'"
- )
+ "This setting controls the SAT library which is used. Valid values are
+ 'minisat2', 'glucose', or 'cadical'"
diff --git src/solvers/CMakeLists.txt src/solvers/CMakeLists.txt
-index f88f9a726..82cbba36e 100644
+index d55ec09..4a6dd4f 100644
--- src/solvers/CMakeLists.txt
+++ src/solvers/CMakeLists.txt
-@@ -55,30 +55,37 @@ list(REMOVE_ITEM sources
+@@ -55,30 +55,35 @@ list(REMOVE_ITEM sources
add_library(solvers ${sources})
+-include("${CBMC_SOURCE_DIR}/../cmake/DownloadProject.cmake")
+if( NOT WITH_SYSTEM_SAT_SOLVER )
-+
- include("${CBMC_SOURCE_DIR}/../cmake/DownloadProject.cmake")
++ include("${CBMC_SOURCE_DIR}/../cmake/DownloadProject.cmake")
+else()
-+message(STATUS "Building solvers with system SAT solver")
++ message(STATUS "Building solvers with system SAT solver")
+endif()
if("${sat_impl}" STREQUAL "minisat2")
@@ -42,39 +42,30 @@ index f88f9a726..82cbba36e 100644
- )
-
- add_subdirectory(${minisat2_SOURCE_DIR} ${minisat2_BINARY_DIR})
-+ target_sources(solvers PRIVATE ${minisat2_source})
-+ if( NOT WITH_SYSTEM_SAT_SOLVER )
-+ # once we upgrade to CMake 3.7 or higher we can specify multiple URLs as a
-+ # fall-back in case the first URL fails (the Makefile-based build retries up
-+ # to 2 times)
-+ download_project(PROJ minisat2
-+ URL
http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
-+ PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/minisat-2.2.1-patch
-+ COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/minisat2_CMakeLists.txt
CMakeLists.txt
-+ URL_MD5 27faa19ee0508660bd6fb7f894646d42
-+ )
-+ add_subdirectory(${minisat2_SOURCE_DIR} ${minisat2_BINARY_DIR})
-+ target_link_libraries(solvers minisat2-condensed)
-+ else()
-+ target_link_libraries(solvers minisat)
-+ endif()
++ target_sources(solvers PRIVATE ${minisat2_source})
++ if( NOT WITH_SYSTEM_SAT_SOLVER )
++ # once we upgrade to CMake 3.7 or higher we can specify multiple URLs as a
++ # fall-back in case the first URL fails (the Makefile-based build retries up
++ # to 2 times)
++ download_project(PROJ minisat2
++ URL
http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
++ PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/minisat-2.2.1-patch
++ COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/minisat2_CMakeLists.txt
CMakeLists.txt
++ URL_MD5 27faa19ee0508660bd6fb7f894646d42
++ )
++ add_subdirectory(${minisat2_SOURCE_DIR} ${minisat2_BINARY_DIR})
++ target_link_libraries(solvers minisat2-condensed)
++ else()
++ target_link_libraries(solvers minisat)
++ endif()
target_compile_definitions(solvers PUBLIC
SATCHECK_MINISAT2 HAVE_MINISAT2 __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS
)
- target_sources(solvers PRIVATE ${minisat2_source})
-
+-
- target_link_libraries(solvers minisat2-condensed)
elseif("${sat_impl}" STREQUAL "glucose")
message(STATUS "Building solvers with glucose")
-@@ -113,5 +120,8 @@ endif()
- # Executable
- add_executable(smt2_solver smt2/smt2_solver.cpp)
- target_link_libraries(smt2_solver solvers)
-+#if("${sat_impl}" STREQUAL "minisat2" AND WITH_SYSTEM_SAT_SOLVER)
-+#target_link_libraries(smt2_solver solvers minisat)
-+#endif()
-
- generic_includes(solvers)
diff --git a/cbmc-signed-char.patch b/cbmc-signed-char.patch
index 79c11dd..a871f96 100644
--- a/cbmc-signed-char.patch
+++ b/cbmc-signed-char.patch
@@ -1,9 +1,9 @@
diff --git unit/util/string_utils/escape_non_alnum.cpp
unit/util/string_utils/escape_non_alnum.cpp
-index 6b1a1b51e..da617a312 100644
+index 147ef17..ebc1f8f 100644
--- unit/util/string_utils/escape_non_alnum.cpp
+++ unit/util/string_utils/escape_non_alnum.cpp
-@@ -18,261 +18,261 @@ TEST_CASE(
- "escape_non_alnum should work with any single byte signed character.",
+@@ -20,267 +20,267 @@ TEST_CASE(
+ "escape_non_alnum should work with any single byte signed character (part
1)",
"[core][utils][string_utils][escape_non_alnum]")
{
- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x00)}) ==
"_00");
@@ -135,134 +135,6 @@ index 6b1a1b51e..da617a312 100644
- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x7D)}) ==
"_7d");
- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x7E)}) ==
"_7e");
- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x7F)}) ==
"_7f");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x80)}) ==
"_80");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x81)}) ==
"_81");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x82)}) ==
"_82");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x83)}) ==
"_83");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x84)}) ==
"_84");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x85)}) ==
"_85");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x86)}) ==
"_86");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x87)}) ==
"_87");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x88)}) ==
"_88");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x89)}) ==
"_89");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x8A)}) ==
"_8a");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x8B)}) ==
"_8b");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x8C)}) ==
"_8c");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x8D)}) ==
"_8d");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x8E)}) ==
"_8e");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x8F)}) ==
"_8f");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x90)}) ==
"_90");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x91)}) ==
"_91");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x92)}) ==
"_92");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x93)}) ==
"_93");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x94)}) ==
"_94");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x95)}) ==
"_95");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x96)}) ==
"_96");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x97)}) ==
"_97");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x98)}) ==
"_98");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x99)}) ==
"_99");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x9A)}) ==
"_9a");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x9B)}) ==
"_9b");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x9C)}) ==
"_9c");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x9D)}) ==
"_9d");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x9E)}) ==
"_9e");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x9F)}) ==
"_9f");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xA0)}) ==
"_a0");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xA1)}) ==
"_a1");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xA2)}) ==
"_a2");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xA3)}) ==
"_a3");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xA4)}) ==
"_a4");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xA5)}) ==
"_a5");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xA6)}) ==
"_a6");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xA7)}) ==
"_a7");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xA8)}) ==
"_a8");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xA9)}) ==
"_a9");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xAA)}) ==
"_aa");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xAB)}) ==
"_ab");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xAC)}) ==
"_ac");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xAD)}) ==
"_ad");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xAE)}) ==
"_ae");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xAF)}) ==
"_af");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xB0)}) ==
"_b0");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xB1)}) ==
"_b1");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xB2)}) ==
"_b2");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xB3)}) ==
"_b3");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xB4)}) ==
"_b4");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xB5)}) ==
"_b5");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xB6)}) ==
"_b6");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xB7)}) ==
"_b7");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xB8)}) ==
"_b8");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xB9)}) ==
"_b9");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xBA)}) ==
"_ba");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xBB)}) ==
"_bb");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xBC)}) ==
"_bc");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xBD)}) ==
"_bd");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xBE)}) ==
"_be");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xBF)}) ==
"_bf");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xC0)}) ==
"_c0");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xC1)}) ==
"_c1");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xC2)}) ==
"_c2");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xC3)}) ==
"_c3");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xC4)}) ==
"_c4");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xC5)}) ==
"_c5");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xC6)}) ==
"_c6");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xC7)}) ==
"_c7");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xC8)}) ==
"_c8");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xC9)}) ==
"_c9");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xCA)}) ==
"_ca");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xCB)}) ==
"_cb");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xCC)}) ==
"_cc");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xCD)}) ==
"_cd");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xCE)}) ==
"_ce");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xCF)}) ==
"_cf");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xD0)}) ==
"_d0");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xD1)}) ==
"_d1");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xD2)}) ==
"_d2");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xD3)}) ==
"_d3");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xD4)}) ==
"_d4");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xD5)}) ==
"_d5");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xD6)}) ==
"_d6");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xD7)}) ==
"_d7");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xD8)}) ==
"_d8");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xD9)}) ==
"_d9");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xDA)}) ==
"_da");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xDB)}) ==
"_db");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xDC)}) ==
"_dc");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xDD)}) ==
"_dd");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xDE)}) ==
"_de");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xDF)}) ==
"_df");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xE0)}) ==
"_e0");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xE1)}) ==
"_e1");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xE2)}) ==
"_e2");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xE3)}) ==
"_e3");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xE4)}) ==
"_e4");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xE5)}) ==
"_e5");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xE6)}) ==
"_e6");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xE7)}) ==
"_e7");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xE8)}) ==
"_e8");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xE9)}) ==
"_e9");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xEA)}) ==
"_ea");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xEB)}) ==
"_eb");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xEC)}) ==
"_ec");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xED)}) ==
"_ed");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xEE)}) ==
"_ee");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xEF)}) ==
"_ef");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xF0)}) ==
"_f0");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xF1)}) ==
"_f1");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xF2)}) ==
"_f2");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xF3)}) ==
"_f3");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xF4)}) ==
"_f4");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xF5)}) ==
"_f5");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xF6)}) ==
"_f6");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xF7)}) ==
"_f7");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xF8)}) ==
"_f8");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xF9)}) ==
"_f9");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xFA)}) ==
"_fa");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xFB)}) ==
"_fb");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xFC)}) ==
"_fc");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xFD)}) ==
"_fd");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xFE)}) ==
"_fe");
-- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xFF)}) ==
"_ff");
+ CHECK(escape_non_alnum({'\x00'}) == "_00");
+ CHECK(escape_non_alnum({'\x01'}) == "_01");
+ CHECK(escape_non_alnum({'\x02'}) == "_02");
@@ -392,6 +264,140 @@ index 6b1a1b51e..da617a312 100644
+ CHECK(escape_non_alnum({'\x7D'}) == "_7d");
+ CHECK(escape_non_alnum({'\x7E'}) == "_7e");
+ CHECK(escape_non_alnum({'\x7F'}) == "_7f");
+ }
+
+ TEST_CASE(
+ "escape_non_alnum should work with any single byte signed character (part
2)",
+ "[core][utils][string_utils][escape_non_alnum]")
+ {
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x80)}) ==
"_80");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x81)}) ==
"_81");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x82)}) ==
"_82");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x83)}) ==
"_83");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x84)}) ==
"_84");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x85)}) ==
"_85");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x86)}) ==
"_86");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x87)}) ==
"_87");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x88)}) ==
"_88");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x89)}) ==
"_89");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x8A)}) ==
"_8a");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x8B)}) ==
"_8b");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x8C)}) ==
"_8c");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x8D)}) ==
"_8d");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x8E)}) ==
"_8e");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x8F)}) ==
"_8f");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x90)}) ==
"_90");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x91)}) ==
"_91");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x92)}) ==
"_92");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x93)}) ==
"_93");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x94)}) ==
"_94");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x95)}) ==
"_95");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x96)}) ==
"_96");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x97)}) ==
"_97");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x98)}) ==
"_98");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x99)}) ==
"_99");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x9A)}) ==
"_9a");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x9B)}) ==
"_9b");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x9C)}) ==
"_9c");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x9D)}) ==
"_9d");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x9E)}) ==
"_9e");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0x9F)}) ==
"_9f");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xA0)}) ==
"_a0");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xA1)}) ==
"_a1");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xA2)}) ==
"_a2");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xA3)}) ==
"_a3");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xA4)}) ==
"_a4");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xA5)}) ==
"_a5");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xA6)}) ==
"_a6");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xA7)}) ==
"_a7");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xA8)}) ==
"_a8");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xA9)}) ==
"_a9");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xAA)}) ==
"_aa");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xAB)}) ==
"_ab");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xAC)}) ==
"_ac");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xAD)}) ==
"_ad");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xAE)}) ==
"_ae");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xAF)}) ==
"_af");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xB0)}) ==
"_b0");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xB1)}) ==
"_b1");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xB2)}) ==
"_b2");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xB3)}) ==
"_b3");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xB4)}) ==
"_b4");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xB5)}) ==
"_b5");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xB6)}) ==
"_b6");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xB7)}) ==
"_b7");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xB8)}) ==
"_b8");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xB9)}) ==
"_b9");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xBA)}) ==
"_ba");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xBB)}) ==
"_bb");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xBC)}) ==
"_bc");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xBD)}) ==
"_bd");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xBE)}) ==
"_be");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xBF)}) ==
"_bf");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xC0)}) ==
"_c0");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xC1)}) ==
"_c1");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xC2)}) ==
"_c2");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xC3)}) ==
"_c3");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xC4)}) ==
"_c4");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xC5)}) ==
"_c5");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xC6)}) ==
"_c6");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xC7)}) ==
"_c7");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xC8)}) ==
"_c8");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xC9)}) ==
"_c9");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xCA)}) ==
"_ca");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xCB)}) ==
"_cb");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xCC)}) ==
"_cc");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xCD)}) ==
"_cd");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xCE)}) ==
"_ce");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xCF)}) ==
"_cf");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xD0)}) ==
"_d0");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xD1)}) ==
"_d1");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xD2)}) ==
"_d2");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xD3)}) ==
"_d3");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xD4)}) ==
"_d4");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xD5)}) ==
"_d5");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xD6)}) ==
"_d6");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xD7)}) ==
"_d7");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xD8)}) ==
"_d8");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xD9)}) ==
"_d9");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xDA)}) ==
"_da");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xDB)}) ==
"_db");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xDC)}) ==
"_dc");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xDD)}) ==
"_dd");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xDE)}) ==
"_de");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xDF)}) ==
"_df");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xE0)}) ==
"_e0");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xE1)}) ==
"_e1");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xE2)}) ==
"_e2");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xE3)}) ==
"_e3");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xE4)}) ==
"_e4");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xE5)}) ==
"_e5");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xE6)}) ==
"_e6");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xE7)}) ==
"_e7");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xE8)}) ==
"_e8");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xE9)}) ==
"_e9");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xEA)}) ==
"_ea");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xEB)}) ==
"_eb");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xEC)}) ==
"_ec");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xED)}) ==
"_ed");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xEE)}) ==
"_ee");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xEF)}) ==
"_ef");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xF0)}) ==
"_f0");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xF1)}) ==
"_f1");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xF2)}) ==
"_f2");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xF3)}) ==
"_f3");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xF4)}) ==
"_f4");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xF5)}) ==
"_f5");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xF6)}) ==
"_f6");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xF7)}) ==
"_f7");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xF8)}) ==
"_f8");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xF9)}) ==
"_f9");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xFA)}) ==
"_fa");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xFB)}) ==
"_fb");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xFC)}) ==
"_fc");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xFD)}) ==
"_fd");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xFE)}) ==
"_fe");
+- CHECK(escape_non_alnum(std::string{static_cast<signed char>(0xFF)}) ==
"_ff");
+ CHECK(escape_non_alnum({'\x80'}) == "_80");
+ CHECK(escape_non_alnum({'\x81'}) == "_81");
+ CHECK(escape_non_alnum({'\x82'}) == "_82");
diff --git a/cbmc.spec b/cbmc.spec
index b2a4d1c..ff83ab3 100644
--- a/cbmc.spec
+++ b/cbmc.spec
@@ -5,7 +5,7 @@
%define _lto_cflags %{nil}
Name: cbmc
-Version: 5.17.0
+Version: 5.24.0
Release: 1%{?dist}
Summary: Bounded Model Checker for ANSI-C and C++ programs
@@ -13,21 +13,26 @@ License: BSD with advertising
URL:
http://www.cprover.org/cbmc/
Source0:
https://github.com/diffblue/%{name}/archive/%{name}-%{version}/%{name}-%{...
-Source1:
https://github.com/vmihalko/%{name}-utils/archive/v%{utils_version}/%{nam...
+Source1:
https://github.com/aufover/%{name}-utils/archive/v%{utils_version}/%{name...
# Adapt to recent versions of glpk
Patch0: %{name}-5.9-glpk.patch
# Regression test regression/cpp/virtual0 is failing - hotfix
-%if 0%{?fedora} > 32
Patch1: %{name}-5.12-fix-f33.patch
-%endif
-# Fedora-specific patch: python => python3 in one test case
-Patch2: %{name}-5.12.6-fix-f33+.patch
-# Use minisat from Fedora
-Patch3: %{name}-minisat.patch
-Patch4: %{name}-32bit-arch-fix.patch
-Patch5: %{name}-signed-char.patch
-
+# Use minisat from Fedora repos
+Patch2: %{name}-minisat.patch
+# Fix compilation on 32 bit architectures
+Patch3: %{name}-32bit-arch-fix.patch
+# Fix compilation of tests
+Patch4: %{name}-signed-char.patch
+# /src/goto-cc/ms_link_cmdline.cpp, use non-reference type 'const string'
+Patch5: %{name}-goto-cc-type-change.patch
+# Fix imcompatibility with glibc 2.33+
+Patch6: %{name}-errno-realpath.patch
+# Skip some c++ tests as cbmc cannot parse some GCC 11 headers
+Patch7: %{name}-f34-fix-build.patch
+# from
https://src.fedoraproject.org/rpms/catch/c/771d2
+Patch8: %{name}-catch2.patch
BuildRequires: bash
BuildRequires: bison
@@ -38,7 +43,9 @@ BuildRequires: gcc-c++
BuildRequires: gdb
BuildRequires: glpk-devel
BuildRequires: graphviz
+BuildRequires: make
BuildRequires: minisat2-devel
+BuildRequires: ninja-build
BuildRequires: zlib-devel
Requires: gcc-c++
@@ -63,10 +70,27 @@ Output conversion utilities for CBMC (GCC like format)
%prep
%setup -T -q -b 1 -n %{name}-utils-%{utils_version}
-%autosetup -p0 -n %{name}-%{name}-%{version}
+%setup -T -q -b 0 -n %{name}-%{name}-%{version}
+
+# FIXME: Upstream the patches
+%patch0 -p0
+%if 0%{?fedora} > 32
+%patch1 -p0
+%endif
+%patch2 -p0
+%ifarch armv7hl i686
+%patch3 -p0
+%endif
+%patch4 -p0
+%patch5 -p0
+%patch6 -p0
+%if 0%{?fedora} > 33
+%patch7 -p0
+%endif
+%patch8 -p0
%build
-%cmake -DWITH_JBMC=OFF -DWITH_SYSTEM_SAT_SOLVER=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
@@ -80,6 +104,9 @@ 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
+# goto-clang is (by default) generating hybrid binary
+ln -s %{_bindir}/goto-cc %{buildroot}%{_bindir}/goto-clang
+
# Feed the debuginfo generator
ln -s xml_y.tab.h src/xmllang/xml_y.tab.hpp
@@ -94,7 +121,7 @@ ln -s xml_y.tab.h src/xmllang/xml_y.tab.hpp
%files
%doc CHANGELOG README.md
%license LICENSE
-%{_bindir}/{cbmc,goto-{analyzer,cc,diff,instrument,gcc,harness,ld}}
+%{_bindir}/*
%{_mandir}/man1/*
%files doc
@@ -107,6 +134,10 @@ ln -s xml_y.tab.h src/xmllang/xml_y.tab.hpp
%changelog
+* Mon Mar 08 2021 Vincent Mihalkovic <vmihalko(a)redhat.com> - 5.24.0-1
+- Add goto-clang for a hybrid binary translation
+- New upstream release
+
* Mon Nov 02 2020 Vincent Mihalkovic <vmihalko(a)redhat.com> - 5.17.0-1
- New upstream release
diff --git a/sources b/sources
index c5ed897..c032c07 100644
--- a/sources
+++ b/sources
@@ -1,2 +1,2 @@
SHA512 (cbmc-utils-1.0.tar.gz) =
a87b423b4dde19fec03d4ee9542c0514134c72ce41af37c1d70c131f0aa844d084ce0bf5a1703694a2709f5f05609e87ce726ee14778ac12cf99109d5a1838d2
-SHA512 (cbmc-5.17.0.tar.gz) =
6ed0e2af634756caa83831e10d29299114add36a3e4bcc602f37443b8e33588aaae12e33066d21cb00f0f1047a60bb87968c0ea7e74742e9e28c7de2407944de
+SHA512 (cbmc-5.24.0.tar.gz) =
3a0fd2aa2256fd16b5ebf62bfa33a9d8708cef49ca6d09eac57f635a8306df8374b790e6813229e1f844c46eddcc3874be6e80931cb9b847f603bf3acf34a7b5