Script 'mail_helper' called by obssrc
Hello community,

here is the log from the commit of package klee for openSUSE:Factory checked in 
at 2023-12-21 23:39:06
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Comparing /work/SRC/openSUSE:Factory/klee (Old)
 and      /work/SRC/openSUSE:Factory/.klee.new.1840 (New)
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

Package is "klee"

Thu Dec 21 23:39:06 2023 rev:37 rq:1134421 version:3.0+20231023

Changes:
--------
--- /work/SRC/openSUSE:Factory/klee/klee.changes        2023-06-23 
21:52:47.430678855 +0200
+++ /work/SRC/openSUSE:Factory/.klee.new.1840/klee.changes      2023-12-21 
23:39:18.736068362 +0100
@@ -1,0 +2,53 @@
+Thu Dec 14 07:40:13 UTC 2023 - jsl...@suse.cz
+
+- Update to version 3.0+20231023:
+  * replace deprecated (as of c++20) std::is_pod with std::trivial &&
+    std::is_standard_layout
+  * Make KDAlloc the default memory allocator
+  * Remove broken experimental optimisation for validity (--cex-cache-exp)
+  * Add code to only keep in the --help menu the KLEE/Kleaver option categories
+  * Move some options to the klee namespace and declare them in
+    OptionCategories.h
+  * Replaced --suppress-external-warnings and --all-external-warnings with
+    --external-call-warnings=none|once-per-function|all.
+  * Combine all `ConstantExpr::toMemory` cases into one.
+  * Using std::memcpy prevents alignment problems and removes an unnecessary
+    special case
+  * Implement getLocationInfo in the same style as getSize
+  * Have CoWPtr::get and CoWPtr::getOwned return pointers instead of references
+  * rename Allocator::location_info to Allocator::locationInfo for consistency
+  * Consistently use ".ktest" when referring to .ktest files in the help menu
+  * Remove parentheses around klee_ intrinsics from the help menu
+  * Fixed a couple of spelling issues in the help menu
+  * Improved help message for --exit-on-error-type=Abort
+  * and more
+- clean up spec file and switch to manual service
+- switch to LLVM 16
+- added patches
+  * 0001-Add-support-to-build-newer-LLVM-versions.patch
+  * 0001-test-disable-failing-tests-with-llvm-15.patch
+  * 0002-Add-support-for-newer-libc-Simplify-path-detection.patch
+  * 0003-Replace-libcxx_include-with-libcxx_includes-for-mult.patch
+  * 0004-Fix-klee-libc-memchr.c-compiler-warning.patch
+  * 0005-Fix-klee_eh_cxx.cpp-compiler-error.patch
+  * 0006-Refactor-invocation-of-old-pass-manager-into-legacy-.patch
+  * 0007-Use-KLEE-s-uClibc-v1.4-as-default-to-support-the-com.patch
+  * 0008-Assume-C-compiler-s-default-standard-is-std-gnu17.patch
+  * 0009-Explicitly-build-KLEE-s-exception-handling-runtime-w.patch
+  * 0010-Explicitly-enable-opaque-pointer-support-for-LLVM-15.patch
+  * 0011-Add-support-for-opaque-pointers.patch
+  * 0012-Fix-test-cases-to-support-opaque-pointers.patch
+  * 0013-Fix-test-case-using-unsupported-CHECK_NEXT-instead-o.patch
+  * 0014-Use-APIs-of-newer-LLVM-versions-instead-of-unsupport.patch
+  * 0015-Add-support-for-Intrinsic-get_rounding-for-LLVM-16.patch
+  * 0016-Add-support-to-aligned_alloc-generated-by-LLVM.patch
+  * 0017-Disable-unsupported-passes-for-newer-LLVM-versions.patch
+  * 0018-Disable-2018-10-30-llvm-pr39177.ll-for-newer-LLVM-ve.patch
+  * 0019-Handle-check-for-thrown-libc-exceptions-more-general.patch
+  * 0020-Update-test-case-for-expressions-using-udiv-urem-sdi.patch
+  * 0021-Support-newer-LLVM-versions-in-lit.patch
+  * 0022-Enable-CI-to-test-newer-LLVM-versions.patch
+- removed patches
+  * 0001-test-disable-until-it-is-fixed.patch (appears to be unnecessary now)
+
+-------------------------------------------------------------------

Old:
----
  0001-test-disable-until-it-is-fixed.patch
  klee-3.0+20230611.obscpio

New:
----
  0001-Add-support-to-build-newer-LLVM-versions.patch
  0001-test-disable-failing-tests-with-llvm-15.patch
  0002-Add-support-for-newer-libc-Simplify-path-detection.patch
  0003-Replace-libcxx_include-with-libcxx_includes-for-mult.patch
  0004-Fix-klee-libc-memchr.c-compiler-warning.patch
  0005-Fix-klee_eh_cxx.cpp-compiler-error.patch
  0006-Refactor-invocation-of-old-pass-manager-into-legacy-.patch
  0007-Use-KLEE-s-uClibc-v1.4-as-default-to-support-the-com.patch
  0008-Assume-C-compiler-s-default-standard-is-std-gnu17.patch
  0009-Explicitly-build-KLEE-s-exception-handling-runtime-w.patch
  0010-Explicitly-enable-opaque-pointer-support-for-LLVM-15.patch
  0011-Add-support-for-opaque-pointers.patch
  0012-Fix-test-cases-to-support-opaque-pointers.patch
  0013-Fix-test-case-using-unsupported-CHECK_NEXT-instead-o.patch
  0014-Use-APIs-of-newer-LLVM-versions-instead-of-unsupport.patch
  0015-Add-support-for-Intrinsic-get_rounding-for-LLVM-16.patch
  0016-Add-support-to-aligned_alloc-generated-by-LLVM.patch
  0017-Disable-unsupported-passes-for-newer-LLVM-versions.patch
  0018-Disable-2018-10-30-llvm-pr39177.ll-for-newer-LLVM-ve.patch
  0019-Handle-check-for-thrown-libc-exceptions-more-general.patch
  0020-Update-test-case-for-expressions-using-udiv-urem-sdi.patch
  0021-Support-newer-LLVM-versions-in-lit.patch
  0022-Enable-CI-to-test-newer-LLVM-versions.patch
  klee-3.0+20231023.obscpio

BETA DEBUG BEGIN:
  Old:- removed patches
  * 0001-test-disable-until-it-is-fixed.patch (appears to be unnecessary now)
BETA DEBUG END:

BETA DEBUG BEGIN:
  New:- added patches
  * 0001-Add-support-to-build-newer-LLVM-versions.patch
  * 0001-test-disable-failing-tests-with-llvm-15.patch
  New:  * 0001-Add-support-to-build-newer-LLVM-versions.patch
  * 0001-test-disable-failing-tests-with-llvm-15.patch
  * 0002-Add-support-for-newer-libc-Simplify-path-detection.patch
  New:  * 0001-test-disable-failing-tests-with-llvm-15.patch
  * 0002-Add-support-for-newer-libc-Simplify-path-detection.patch
  * 0003-Replace-libcxx_include-with-libcxx_includes-for-mult.patch
  New:  * 0002-Add-support-for-newer-libc-Simplify-path-detection.patch
  * 0003-Replace-libcxx_include-with-libcxx_includes-for-mult.patch
  * 0004-Fix-klee-libc-memchr.c-compiler-warning.patch
  New:  * 0003-Replace-libcxx_include-with-libcxx_includes-for-mult.patch
  * 0004-Fix-klee-libc-memchr.c-compiler-warning.patch
  * 0005-Fix-klee_eh_cxx.cpp-compiler-error.patch
  New:  * 0004-Fix-klee-libc-memchr.c-compiler-warning.patch
  * 0005-Fix-klee_eh_cxx.cpp-compiler-error.patch
  * 0006-Refactor-invocation-of-old-pass-manager-into-legacy-.patch
  New:  * 0005-Fix-klee_eh_cxx.cpp-compiler-error.patch
  * 0006-Refactor-invocation-of-old-pass-manager-into-legacy-.patch
  * 0007-Use-KLEE-s-uClibc-v1.4-as-default-to-support-the-com.patch
  New:  * 0006-Refactor-invocation-of-old-pass-manager-into-legacy-.patch
  * 0007-Use-KLEE-s-uClibc-v1.4-as-default-to-support-the-com.patch
  * 0008-Assume-C-compiler-s-default-standard-is-std-gnu17.patch
  New:  * 0007-Use-KLEE-s-uClibc-v1.4-as-default-to-support-the-com.patch
  * 0008-Assume-C-compiler-s-default-standard-is-std-gnu17.patch
  * 0009-Explicitly-build-KLEE-s-exception-handling-runtime-w.patch
  New:  * 0008-Assume-C-compiler-s-default-standard-is-std-gnu17.patch
  * 0009-Explicitly-build-KLEE-s-exception-handling-runtime-w.patch
  * 0010-Explicitly-enable-opaque-pointer-support-for-LLVM-15.patch
  New:  * 0009-Explicitly-build-KLEE-s-exception-handling-runtime-w.patch
  * 0010-Explicitly-enable-opaque-pointer-support-for-LLVM-15.patch
  * 0011-Add-support-for-opaque-pointers.patch
  New:  * 0010-Explicitly-enable-opaque-pointer-support-for-LLVM-15.patch
  * 0011-Add-support-for-opaque-pointers.patch
  * 0012-Fix-test-cases-to-support-opaque-pointers.patch
  New:  * 0011-Add-support-for-opaque-pointers.patch
  * 0012-Fix-test-cases-to-support-opaque-pointers.patch
  * 0013-Fix-test-case-using-unsupported-CHECK_NEXT-instead-o.patch
  New:  * 0012-Fix-test-cases-to-support-opaque-pointers.patch
  * 0013-Fix-test-case-using-unsupported-CHECK_NEXT-instead-o.patch
  * 0014-Use-APIs-of-newer-LLVM-versions-instead-of-unsupport.patch
  New:  * 0013-Fix-test-case-using-unsupported-CHECK_NEXT-instead-o.patch
  * 0014-Use-APIs-of-newer-LLVM-versions-instead-of-unsupport.patch
  * 0015-Add-support-for-Intrinsic-get_rounding-for-LLVM-16.patch
  New:  * 0014-Use-APIs-of-newer-LLVM-versions-instead-of-unsupport.patch
  * 0015-Add-support-for-Intrinsic-get_rounding-for-LLVM-16.patch
  * 0016-Add-support-to-aligned_alloc-generated-by-LLVM.patch
  New:  * 0015-Add-support-for-Intrinsic-get_rounding-for-LLVM-16.patch
  * 0016-Add-support-to-aligned_alloc-generated-by-LLVM.patch
  * 0017-Disable-unsupported-passes-for-newer-LLVM-versions.patch
  New:  * 0016-Add-support-to-aligned_alloc-generated-by-LLVM.patch
  * 0017-Disable-unsupported-passes-for-newer-LLVM-versions.patch
  * 0018-Disable-2018-10-30-llvm-pr39177.ll-for-newer-LLVM-ve.patch
  New:  * 0017-Disable-unsupported-passes-for-newer-LLVM-versions.patch
  * 0018-Disable-2018-10-30-llvm-pr39177.ll-for-newer-LLVM-ve.patch
  * 0019-Handle-check-for-thrown-libc-exceptions-more-general.patch
  New:  * 0018-Disable-2018-10-30-llvm-pr39177.ll-for-newer-LLVM-ve.patch
  * 0019-Handle-check-for-thrown-libc-exceptions-more-general.patch
  * 0020-Update-test-case-for-expressions-using-udiv-urem-sdi.patch
  New:  * 0019-Handle-check-for-thrown-libc-exceptions-more-general.patch
  * 0020-Update-test-case-for-expressions-using-udiv-urem-sdi.patch
  * 0021-Support-newer-LLVM-versions-in-lit.patch
  New:  * 0020-Update-test-case-for-expressions-using-udiv-urem-sdi.patch
  * 0021-Support-newer-LLVM-versions-in-lit.patch
  * 0022-Enable-CI-to-test-newer-LLVM-versions.patch
  New:  * 0021-Support-newer-LLVM-versions-in-lit.patch
  * 0022-Enable-CI-to-test-newer-LLVM-versions.patch
- removed patches
BETA DEBUG END:

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

Other differences:
------------------
++++++ klee.spec ++++++
--- /var/tmp/diff_new_pack.xFDEff/_old  2023-12-21 23:39:19.556098307 +0100
+++ /var/tmp/diff_new_pack.xFDEff/_new  2023-12-21 23:39:19.556098307 +0100
@@ -16,8 +16,7 @@
 #
 
 
-%define llvm_version_major 14
-%define llvm_version %{llvm_version_major}
+%define llvm_version 16
 
 %ifarch x86_64
 %define with_uclibc 1
@@ -31,14 +30,37 @@
 Summary:        LLVM Execution Engine
 License:        NCSA
 Group:          Development/Languages/Other
-Version:        3.0+20230611
+Version:        3.0+20231023
 Release:        0
 URL:            http://klee.github.io/
 Source0:        %{name}-%{version}.tar.xz
 Source1:        %{name}-rpmlintrc
-Source2:        
https://raw.githubusercontent.com/llvm/llvm-project/llvmorg-%{llvm_version_major}.0.0/llvm/utils/not/not.cpp
-Source3:        
https://raw.githubusercontent.com/llvm/llvm-project/llvmorg-%{llvm_version_major}.0.0/llvm/utils/FileCheck/FileCheck.cpp
-Patch0:         0001-test-disable-until-it-is-fixed.patch
+Source2:        
https://raw.githubusercontent.com/llvm/llvm-project/llvmorg-%{llvm_version}.0.0/llvm/utils/not/not.cpp
+Source3:        
https://raw.githubusercontent.com/llvm/llvm-project/llvmorg-%{llvm_version}.0.0/llvm/utils/FileCheck/FileCheck.cpp
+Patch1:         0001-Add-support-to-build-newer-LLVM-versions.patch
+Patch2:         0002-Add-support-for-newer-libc-Simplify-path-detection.patch
+Patch3:         0003-Replace-libcxx_include-with-libcxx_includes-for-mult.patch
+Patch4:         0004-Fix-klee-libc-memchr.c-compiler-warning.patch
+Patch5:         0005-Fix-klee_eh_cxx.cpp-compiler-error.patch
+Patch6:         0006-Refactor-invocation-of-old-pass-manager-into-legacy-.patch
+Patch7:         0007-Use-KLEE-s-uClibc-v1.4-as-default-to-support-the-com.patch
+Patch8:         0008-Assume-C-compiler-s-default-standard-is-std-gnu17.patch
+Patch9:         0009-Explicitly-build-KLEE-s-exception-handling-runtime-w.patch
+Patch10:        0010-Explicitly-enable-opaque-pointer-support-for-LLVM-15.patch
+Patch11:        0011-Add-support-for-opaque-pointers.patch
+Patch12:        0012-Fix-test-cases-to-support-opaque-pointers.patch
+Patch13:        0013-Fix-test-case-using-unsupported-CHECK_NEXT-instead-o.patch
+Patch14:        0014-Use-APIs-of-newer-LLVM-versions-instead-of-unsupport.patch
+Patch15:        0015-Add-support-for-Intrinsic-get_rounding-for-LLVM-16.patch
+Patch16:        0016-Add-support-to-aligned_alloc-generated-by-LLVM.patch
+Patch17:        0017-Disable-unsupported-passes-for-newer-LLVM-versions.patch
+Patch18:        0018-Disable-2018-10-30-llvm-pr39177.ll-for-newer-LLVM-ve.patch
+Patch19:        0019-Handle-check-for-thrown-libc-exceptions-more-general.patch
+Patch20:        0020-Update-test-case-for-expressions-using-udiv-urem-sdi.patch
+Patch21:        0021-Support-newer-LLVM-versions-in-lit.patch
+Patch22:        0022-Enable-CI-to-test-newer-LLVM-versions.patch
+Patch100:       0001-test-disable-failing-tests-with-llvm-15.patch
+
 BuildRequires:  clang%{llvm_version}
 BuildRequires:  cmake
 BuildRequires:  gperftools-devel

++++++ 0001-Add-support-to-build-newer-LLVM-versions.patch ++++++
From: Martin Nowack <m.now...@imperial.ac.uk>
Date: Thu, 12 Oct 2023 10:23:34 +0100
Subject: Add support to build newer LLVM versions
Patch-mainline: no
References: llvm16

`-DLLVM_ENABLE_PROJECTS` does not include runtimes anymore,
instead a `-DLLVM_ENABLE_RUNTIMES` should be used in addition

Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 scripts/build/p-libcxx.inc | 29 ++++++++++++++++++++++-------
 scripts/build/p-llvm.inc   | 21 +++++++++++++--------
 2 files changed, 35 insertions(+), 15 deletions(-)

diff --git a/scripts/build/p-libcxx.inc b/scripts/build/p-libcxx.inc
index 641fad61..b0263c00 100644
--- a/scripts/build/p-libcxx.inc
+++ b/scripts/build/p-libcxx.inc
@@ -30,7 +30,6 @@ build_libcxx() {
   local LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}"
 
   local cmake_flags=(
-   "-DLLVM_ENABLE_PROJECTS=libcxx;libcxxabi"
    "-DLLVM_ENABLE_THREADS:BOOL=OFF"
    "-DLIBCXX_ENABLE_THREADS:BOOL=OFF"
    "-DLIBCXX_ENABLE_SHARED:BOOL=ON"
@@ -40,6 +39,13 @@ build_libcxx() {
   )
 
   # Static ABI libraries are not supported under OS X
+  if [[ "${LLVM_VERSION_SHORT}" -ge "14" ]]; then
+    cmake_flags+=("-DLLVM_ENABLE_RUNTIMES=libcxx;libcxxabi")
+    cmake_flags+=("-DLLVM_ENABLE_PROJECTS=")
+    cmake_flags+=("-DLLVM_ENABLE_PROJECTS_USED:BOOL=ON")
+  else
+    cmake_flags+=("-DLLVM_ENABLE_PROJECTS=libcxx;libcxxabi")
+  fi
   if [[ "${OS}" == "osx" ]]; then
     cmake_flags+=("-DLIBCXX_ENABLE_STATIC_ABI_LIBRARY:BOOL=OFF")
   else
@@ -53,7 +59,11 @@ build_libcxx() {
     export LLVM_COMPILER_PATH="$(dirname "${BITCODE_CC}")"
 
     cmake "${cmake_flags[@]}" "${LIBCXX_SRC}/llvm"
-    make cxx -j$(nproc) || make cxx
+   if [[ "${LLVM_VERSION_SHORT}" -ge "14" ]]; then
+     make runtimes - j"$(nproc)" || make cxx || return 1
+   else
+     make cxx - j"$(nproc)" || make cxx || return 1
+   fi
   )
 }
 
@@ -65,19 +75,24 @@ install_libcxx() {
     export LLVM_COMPILER=clang
     export LLVM_COMPILER_PATH="$(dirname "${BITCODE_CC}")"
 
-    cd "${LIBCXX_BUILD}/projects"
-    make install
+    if [[ "${LLVM_VERSION_SHORT}" -ge "14" ]]; then
+      cd "${LIBCXX_BUILD}/runtimes" || return 1
+      make install || return 1
+    else
+      cd "${LIBCXX_BUILD}/projects" || return 1
+      make install || return 1
+    fi
 
     local libraries
 
     if [[ "${OS}" == "osx" ]]; then
-      libraries=("${LIBCXX_INSTALL}"/lib/lib*.dylib)
+      libraries=("${LIBCXX_INSTALL}"/lib/*/lib*.dylib)
     else
-      libraries=("${LIBCXX_INSTALL}"/lib/lib*.so)
+      libraries=("${LIBCXX_INSTALL}"/lib/*/lib*.so)
     fi
 
     local LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}"
-    libraries+=("${LIBCXX_INSTALL}"/lib/lib*.a)
+    libraries+=("${LIBCXX_INSTALL}"/lib/*/lib*.a)
 
 
     for p in "${libraries[@]}" ; do
diff --git a/scripts/build/p-llvm.inc b/scripts/build/p-llvm.inc
index abf895ae..462d69f5 100644
--- a/scripts/build/p-llvm.inc
+++ b/scripts/build/p-llvm.inc
@@ -174,16 +174,21 @@ configure_llvm() {
   )
 
   if [[ "${SANITIZER_BUILD:-}" == "memory" ]]; then
-    # We have to build without libunwind if RTTI is disables
+    # We have to build without libunwind if RTTI is disabled
     CONFIG+=("-DLLVM_ENABLE_PROJECTS=${ENABLED_LLVM_PROJECTS}")
   else
-      CONFIG+=(
-          "-DLLVM_BUILD_LLVM_DYLIB:BOOL=ON"
-          "-DLLVM_LINK_LLVM_DYLIB:BOOL=ON"
-          "-DLLVM_BUILD_STATIC:BOOL=OFF"
-          "-DLIBCLANG_BUILD_STATIC:BOOL=OFF"
-      )
-      
CONFIG+=("-DLLVM_ENABLE_PROJECTS=${ENABLED_LLVM_PROJECTS};libcxx;libcxxabi;libunwind")
+    CONFIG+=(
+        "-DLLVM_BUILD_LLVM_DYLIB:BOOL=ON"
+        "-DLLVM_LINK_LLVM_DYLIB:BOOL=ON"
+        "-DLLVM_BUILD_STATIC:BOOL=OFF"
+        "-DLIBCLANG_BUILD_STATIC:BOOL=OFF"
+    )
+    if [[ "${LLVM_VERSION_SHORT}" -ge "14" ]]; then
+      CONFIG+=("-DLLVM_ENABLE_PROJECTS=${ENABLED_LLVM_PROJECTS}")
+      CONFIG+=("-DLLVM_ENABLE_RUNTIMES=libcxx;libcxxabi")
+    else
+      
CONFIG+=("-DLLVM_ENABLE_PROJECTS=${ENABLED_LLVM_PROJECTS};libcxx;libcxxabi")
+    fi
   fi
 
   if [[ -n ${SANITIZER_BUILD} ]]; then
-- 
2.43.0


++++++ 0001-test-disable-failing-tests-with-llvm-15.patch ++++++
From: Jiri Slaby <jsl...@suse.cz>
Date: Thu, 14 Dec 2023 10:25:08 +0100
Subject: test: disable failing tests with llvm 15
Patch-mainline: no
References: llvm16

This should be solved, but until then, disable these temporarily.

Links: https://github.com/klee/klee/pull/1664#issuecomment-1855364303
Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 test/Feature/VarArgByVal.c              | 2 +-
 test/Runtime/POSIX/DirConsistency.c     | 1 +
 test/Runtime/POSIX/SymFileConsistency.c | 1 +
 3 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/test/Feature/VarArgByVal.c b/test/Feature/VarArgByVal.c
index 7b979f61..582b584f 100644
--- a/test/Feature/VarArgByVal.c
+++ b/test/Feature/VarArgByVal.c
@@ -1,4 +1,4 @@
-// REQUIRES: geq-llvm-15.0
+// REQUIRES: lt-llvm-15.0
 /* This test checks that KLEE correctly handles variadic arguments with the
    byval attribute */
 
diff --git a/test/Runtime/POSIX/DirConsistency.c 
b/test/Runtime/POSIX/DirConsistency.c
index 5d7e47a1..9183db24 100644
--- a/test/Runtime/POSIX/DirConsistency.c
+++ b/test/Runtime/POSIX/DirConsistency.c
@@ -1,3 +1,4 @@
+// REQUIRES: lt-llvm-15.0
 // RUN: %clang %s -emit-llvm %O0opt -c -g -o %t.bc
 // RUN: rm -rf %t.klee-out %t.klee-out-tmp
 // RUN: %gentmp %t.klee-out-tmp
diff --git a/test/Runtime/POSIX/SymFileConsistency.c 
b/test/Runtime/POSIX/SymFileConsistency.c
index d97f65f0..e2b8b9a8 100644
--- a/test/Runtime/POSIX/SymFileConsistency.c
+++ b/test/Runtime/POSIX/SymFileConsistency.c
@@ -1,4 +1,5 @@
 // REQUIRES: posix-runtime
+// REQUIRES: lt-llvm-15.0
 // RUN: %clang %s -emit-llvm %O0opt -c -g -o %t.bc
 // RUN: rm -rf %t.klee-out-tmp
 // RUN: %klee --output-dir=%t.klee-out-tmp --libc=uclibc --posix-runtime 
--exit-on-error %t.bc --sym-files 1 1 > %t1.log
-- 
2.43.0


++++++ 0002-Add-support-for-newer-libc-Simplify-path-detection.patch ++++++
From: Martin Nowack <m.now...@imperial.ac.uk>
Date: Thu, 12 Oct 2023 10:28:42 +0100
Subject: Add support for newer `libc++`; Simplify path detection
Patch-mainline: no
References: llvm16

`libc++` include headers are now split between platform dependent and
platform independent code.

Before, only include files for the platform independent code were
considered. Add support to automatically find platform dependent
includes as well.

Simplify the detection of libraries and paths.

Instead of pointing to the `v1` directory, pointing to the include
directory for `-DKLEE_LIBCXX_INCLUDE_PATH` is enough.

Update build script to support this as well.

Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 CMakeLists.txt                     | 65 +++++++++++++-----------------
 runtime/klee-eh-cxx/CMakeLists.txt |  8 +++-
 scripts/build/p-klee.inc           |  2 +-
 3 files changed, 37 insertions(+), 38 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 19e9fc06..6c55eae9 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -496,51 +496,44 @@ option(ENABLE_KLEE_LIBCXX "Enable libc++ for klee" OFF)
 if (ENABLE_KLEE_LIBCXX)
   message(STATUS "klee-libc++ support enabled")
   set(SUPPORT_KLEE_LIBCXX 1) # For config.h
-  set(KLEE_LIBCXX_DIR "" CACHE PATH "Path to directory containing libc++ 
shared object (bitcode)")
-  if (NOT EXISTS "${KLEE_LIBCXX_DIR}")
-    message(FATAL_ERROR
-      "KLEE_LIBCXX_DIR (\"${KLEE_LIBCXX_DIR}\") does not exist.\n"
-      "Try passing -DKLEE_LIBCXX_DIR=<path> to CMake where <path> is the path"
-      "to the directory containing the libc++ shared object file (as 
bitcode).")
-  endif()
 
-  set(KLEE_LIBCXX_INCLUDE_DIR "" CACHE PATH "Path to libc++ include directory")
-  if (NOT EXISTS "${KLEE_LIBCXX_INCLUDE_DIR}")
-    message(FATAL_ERROR
-      "KLEE_LIBCXX_INCLUDE_DIR (\"${KLEE_LIBCXX_INCLUDE_DIR}\") does not 
exist.\n"
-      "Try passing -DKLEE_LIBCXX_INCLUDE_DIR=<path> to CMake where <path> is 
the"
-      "libc++ include directory.")
-  endif()
-  message(STATUS "Use libc++ include path: \"${KLEE_LIBCXX_INCLUDE_DIR}\"")
-
-  # Find the library bitcode archive
-
-  # Check for static first
-  set(KLEE_LIBCXX_BC_NAME "libc++.bca")
-  set(KLEE_LIBCXX_BC_PATH "${KLEE_LIBCXX_DIR}/lib/${KLEE_LIBCXX_BC_NAME}")
-  if (NOT EXISTS "${KLEE_LIBCXX_BC_PATH}")
-    # Check for dynamic so lib
-    set(KLEE_LIBCXX_BC_NAME "libc++.so.bc")
-    set(KLEE_LIBCXX_BC_PATH "${KLEE_LIBCXX_DIR}/lib/${KLEE_LIBCXX_BC_NAME}")
-    if (NOT EXISTS "${KLEE_LIBCXX_BC_PATH}")
-      set(KLEE_LIBCXX_BC_NAME "libc++.dylib.bc")
-      set(KLEE_LIBCXX_BC_PATH "${KLEE_LIBCXX_DIR}/lib/${KLEE_LIBCXX_BC_NAME}")
-      if (NOT EXISTS "${KLEE_LIBCXX_BC_PATH}")
-        message(FATAL_ERROR
-          "libc++ library not found at \"${KLEE_LIBCXX_DIR}\"")
-      endif()
-    endif()
-  endif()
+  find_file(KLEE_LIBCXX_BC_PATH
+          NAMES libc++.bca libc++.so.bc libc++.dylib.bc
+          DOC "Path to directory containing libc++ shared object (bitcode)"
+          PATH_SUFFIXES "lib" "lib/x86_64-unknown-linux-gnu"
+          HINTS ${KLEE_LIBCXX_DIR}
+          REQUIRED
+  )
   message(STATUS "Found libc++ library: \"${KLEE_LIBCXX_BC_PATH}\"")
 
+  find_path(KLEE_LIBCXX_PLATFORM_INCLUDE_PATH
+          NAMES __config_site #We are searching for a platform-specific C++ 
library header called `__config_site`
+          DOC "Path to platform-specific libc++ include directory"
+          PATH_SUFFIXES "x86_64-unknown-linux-gnu/c++/v1" 
"include/x86_64-unknown-linux-gnu/c++/v1"
+          HINTS ${KLEE_LIBCXX_INCLUDE_DIR}
+          NO_DEFAULT_PATH # Make sure we don't pick-up the standard library's 
path
+  )
+
+  find_path(KLEE_LIBCXX_INCLUDE_PATH
+          NAMES cerrno #We are searching for a C++ library header called 
`cerrno`
+          DOC "Path to libc++ include directory"
+          PATH_SUFFIXES "c++/v1" "include/c++/v1"
+          HINTS ${KLEE_LIBCXX_INCLUDE_DIR}
+          REQUIRED
+          NO_DEFAULT_PATH # Make sure we don't pick-up the standard library's 
path
+  )
+
+  message(STATUS "Found libc++ include path: ${KLEE_LIBCXX_INCLUDE_PATH} and 
${KLEE_LIBCXX_PLATFORM_INCLUDE_PATH} ")
+
+
   # Copy KLEE_LIBCXX_BC_PATH so KLEE can find it where it is expected.
   file(MAKE_DIRECTORY "${KLEE_RUNTIME_DIRECTORY}")
   execute_process(COMMAND ${CMAKE_COMMAND} -E copy
     "${KLEE_LIBCXX_BC_PATH}"
-    "${KLEE_RUNTIME_DIRECTORY}/${KLEE_LIBCXX_BC_NAME}"
+    "${KLEE_RUNTIME_DIRECTORY}/${KLEE_LIBCXX_BC_PATH}"
   )
   list(APPEND KLEE_COMPONENT_CXX_DEFINES
-    -DKLEE_LIBCXX_BC_NAME=\"${KLEE_LIBCXX_BC_NAME}\")
+    -DKLEE_LIBCXX_BC_NAME=\"${KLEE_LIBCXX_BC_PATH}\")
 
 else()
   message(STATUS "libc++ support disabled")
diff --git a/runtime/klee-eh-cxx/CMakeLists.txt 
b/runtime/klee-eh-cxx/CMakeLists.txt
index e016757b..470e3f0a 100644
--- a/runtime/klee-eh-cxx/CMakeLists.txt
+++ b/runtime/klee-eh-cxx/CMakeLists.txt
@@ -16,8 +16,14 @@ set(ADDITIONAL_CXX_FLAGS
         -nostdinc++
         -I "${KLEE_LIBCXXABI_SRC_DIR}/src"
         -I "${KLEE_LIBCXXABI_SRC_DIR}/include"
-        -I "${KLEE_LIBCXX_INCLUDE_DIR}"
+        -I "${KLEE_LIBCXX_INCLUDE_PATH}"
+)
+
+if (KLEE_LIBCXX_PLATFORM_INCLUDE_PATH)
+        list(APPEND ADDITIONAL_CXX_FLAGS
+                -I "${KLEE_LIBCXX_PLATFORM_INCLUDE_PATH}"
         )
+endif ()
 # Build it
 include("${CMAKE_SOURCE_DIR}/cmake/compile_bitcode_library.cmake")
 prefix_with_path("${SRC_FILES}" "${CMAKE_CURRENT_SOURCE_DIR}/" prefixed_files)
diff --git a/scripts/build/p-klee.inc b/scripts/build/p-klee.inc
index 82dedeaa..b7384b91 100644
--- a/scripts/build/p-klee.inc
+++ b/scripts/build/p-klee.inc
@@ -49,7 +49,7 @@ if [ "${USE_LIBCXX}" -eq 1 ]; then
   CMAKE_ARGUMENTS+=(
     "-DENABLE_KLEE_LIBCXX=TRUE"
     "-DKLEE_LIBCXX_DIR=${LIBCXX_INSTALL}"
-    "-DKLEE_LIBCXX_INCLUDE_DIR=${LIBCXX_INSTALL}/include/c++/v1"
+    "-DKLEE_LIBCXX_INCLUDE_DIR=${LIBCXX_INSTALL}/include/"
     "-DENABLE_KLEE_EH_CXX=TRUE"
     "-DKLEE_LIBCXXABI_SRC_DIR=${LIBCXX_SRC}/libcxxabi"
   )
-- 
2.43.0


++++++ 0003-Replace-libcxx_include-with-libcxx_includes-for-mult.patch ++++++
From: Martin Nowack <m.now...@imperial.ac.uk>
Date: Thu, 12 Oct 2023 10:32:32 +0100
Subject: Replace `%libcxx_include` with `%libcxx_includes` for multi-include
 directories
Patch-mainline: no
References: llvm16

To support multiple include directories for c++ header files, use
`%libcxx_includes`. This string contains the `-I` compiler directive for
each include path as well.

Update test cases to use new directive.

Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 test/CXX/symex/libc++/atexit.cpp                             | 2 +-
 test/CXX/symex/libc++/can_catch_test.cpp                     | 2 +-
 test/CXX/symex/libc++/catch_recover.cpp                      | 2 +-
 .../symex/libc++/catch_with_adjusted_exception_pointer.cpp   | 2 +-
 test/CXX/symex/libc++/cout.cpp                               | 2 +-
 test/CXX/symex/libc++/cout_sym.cpp                           | 2 +-
 test/CXX/symex/libc++/dynamic_cast.cpp                       | 2 +-
 test/CXX/symex/libc++/exception.cpp                          | 2 +-
 test/CXX/symex/libc++/exception_inheritance.cpp              | 2 +-
 test/CXX/symex/libc++/general_catch.cpp                      | 2 +-
 test/CXX/symex/libc++/landingpad.cpp                         | 2 +-
 test/CXX/symex/libc++/multi_throw.cpp                        | 2 +-
 test/CXX/symex/libc++/multi_unwind.cpp                       | 2 +-
 test/CXX/symex/libc++/nested.cpp                             | 2 +-
 test/CXX/symex/libc++/nested_fail.cpp                        | 2 +-
 test/CXX/symex/libc++/rethrow.cpp                            | 2 +-
 test/CXX/symex/libc++/simple_exception.cpp                   | 2 +-
 test/CXX/symex/libc++/simple_exception_fail.cpp              | 2 +-
 test/CXX/symex/libc++/symbolic_exception.cpp                 | 2 +-
 test/CXX/symex/libc++/throw_specifiers.cpp                   | 2 +-
 test/CXX/symex/libc++/throwing_exception_destructor.cpp      | 2 +-
 test/CXX/symex/libc++/uncaught_exception.cpp                 | 2 +-
 test/CXX/symex/libc++/vector.cpp                             | 2 +-
 test/lit.cfg                                                 | 5 ++++-
 test/lit.site.cfg.in                                         | 4 +++-
 25 files changed, 30 insertions(+), 25 deletions(-)

diff --git a/test/CXX/symex/libc++/atexit.cpp b/test/CXX/symex/libc++/atexit.cpp
index fa8df475..d084958b 100644
--- a/test/CXX/symex/libc++/atexit.cpp
+++ b/test/CXX/symex/libc++/atexit.cpp
@@ -2,7 +2,7 @@
 // Disabling msan because it times out on CI
 // REQUIRES: libcxx
 // REQUIRES: uclibc
-// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g 
-nostdinc++ -o %t1.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g 
-nostdinc++ -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | 
FileCheck %s
 
diff --git a/test/CXX/symex/libc++/can_catch_test.cpp 
b/test/CXX/symex/libc++/can_catch_test.cpp
index c70d14a2..4c59c126 100644
--- a/test/CXX/symex/libc++/can_catch_test.cpp
+++ b/test/CXX/symex/libc++/can_catch_test.cpp
@@ -1,7 +1,7 @@
 // REQUIRES: uclibc
 // REQUIRES: libcxx
 // REQUIRES: eh-cxx
-// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c -I "%libcxx_include" -g 
-nostdinc++ -o %t.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c %libcxx_includes -g 
-nostdinc++ -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error --libcxx --libc=uclibc 
%t.bc 2>&1 | FileCheck %s
 
diff --git a/test/CXX/symex/libc++/catch_recover.cpp 
b/test/CXX/symex/libc++/catch_recover.cpp
index c77bea91..8eee326a 100644
--- a/test/CXX/symex/libc++/catch_recover.cpp
+++ b/test/CXX/symex/libc++/catch_recover.cpp
@@ -2,7 +2,7 @@
 // Disabling msan because it times out on CI
 // REQUIRES: libcxx
 // REQUIRES: eh-cxx
-// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g 
-nostdinc++ -o %t1.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g 
-nostdinc++ -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | 
FileCheck %s
 
diff --git a/test/CXX/symex/libc++/catch_with_adjusted_exception_pointer.cpp 
b/test/CXX/symex/libc++/catch_with_adjusted_exception_pointer.cpp
index e3bf08ad..57751b23 100644
--- a/test/CXX/symex/libc++/catch_with_adjusted_exception_pointer.cpp
+++ b/test/CXX/symex/libc++/catch_with_adjusted_exception_pointer.cpp
@@ -1,7 +1,7 @@
 // REQUIRES: uclibc
 // REQUIRES: libcxx
 // REQUIRES: eh-cxx
-// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c -I "%libcxx_include" -g 
-nostdinc++ -o %t.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c %libcxx_includes -g 
-nostdinc++ -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error --libcxx --libc=uclibc 
%t.bc 2>&1 | FileCheck %s
 
diff --git a/test/CXX/symex/libc++/cout.cpp b/test/CXX/symex/libc++/cout.cpp
index 62cd0406..d845a1ea 100644
--- a/test/CXX/symex/libc++/cout.cpp
+++ b/test/CXX/symex/libc++/cout.cpp
@@ -2,7 +2,7 @@
 // Disabling msan because it times out on CI
 // REQUIRES: libcxx
 // REQUIRES: uclibc
-// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g 
-nostdinc++ -o %t1.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g 
-nostdinc++ -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | 
FileCheck %s
 
diff --git a/test/CXX/symex/libc++/cout_sym.cpp 
b/test/CXX/symex/libc++/cout_sym.cpp
index 177c3ed7..69420ac9 100644
--- a/test/CXX/symex/libc++/cout_sym.cpp
+++ b/test/CXX/symex/libc++/cout_sym.cpp
@@ -2,7 +2,7 @@
 // Disabling msan because it times out on CI
 // REQUIRES: libcxx
 // REQUIRES: uclibc
-// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g 
-nostdinc++ -o %t1.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g 
-nostdinc++ -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | 
FileCheck %s
 
diff --git a/test/CXX/symex/libc++/dynamic_cast.cpp 
b/test/CXX/symex/libc++/dynamic_cast.cpp
index a2fc8b82..f8a039ce 100644
--- a/test/CXX/symex/libc++/dynamic_cast.cpp
+++ b/test/CXX/symex/libc++/dynamic_cast.cpp
@@ -2,7 +2,7 @@
 // Disabling msan because it times out on CI
 // REQUIRES: libcxx
 // REQUIRES: uclibc
-// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g 
-nostdinc++ -o %t1.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g 
-nostdinc++ -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc
 
diff --git a/test/CXX/symex/libc++/exception.cpp 
b/test/CXX/symex/libc++/exception.cpp
index 4d6805f6..c36db2d9 100644
--- a/test/CXX/symex/libc++/exception.cpp
+++ b/test/CXX/symex/libc++/exception.cpp
@@ -2,7 +2,7 @@
 // Disabling msan because it times out on CI
 // REQUIRES: libcxx
 // REQUIRES: eh-cxx
-// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g 
-nostdinc++ -o %t1.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g 
-nostdinc++ -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | 
FileCheck %s
 
diff --git a/test/CXX/symex/libc++/exception_inheritance.cpp 
b/test/CXX/symex/libc++/exception_inheritance.cpp
index ca207eb4..4551bc18 100644
--- a/test/CXX/symex/libc++/exception_inheritance.cpp
+++ b/test/CXX/symex/libc++/exception_inheritance.cpp
@@ -1,7 +1,7 @@
 // REQUIRES: uclibc
 // REQUIRES: libcxx
 // REQUIRES: eh-cxx
-// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c -I "%libcxx_include" -g 
-nostdinc++ -o %t.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c %libcxx_includes -g 
-nostdinc++ -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error --libcxx --libc=uclibc 
%t.bc 2>&1 | FileCheck %s
 
diff --git a/test/CXX/symex/libc++/general_catch.cpp 
b/test/CXX/symex/libc++/general_catch.cpp
index c544f7a3..eb045d16 100644
--- a/test/CXX/symex/libc++/general_catch.cpp
+++ b/test/CXX/symex/libc++/general_catch.cpp
@@ -2,7 +2,7 @@
 // Disabling msan because it times out on CI
 // REQUIRES: libcxx
 // REQUIRES: eh-cxx
-// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g 
-nostdinc++ -o %t1.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g 
-nostdinc++ -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | 
FileCheck %s
 
diff --git a/test/CXX/symex/libc++/landingpad.cpp 
b/test/CXX/symex/libc++/landingpad.cpp
index 13dd6bc4..c23b8ee2 100644
--- a/test/CXX/symex/libc++/landingpad.cpp
+++ b/test/CXX/symex/libc++/landingpad.cpp
@@ -4,7 +4,7 @@
 // REQUIRES: uclibc
 // REQUIRES: libcxx
 // REQUIRES: eh-cxx
-// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c -I "%libcxx_include" -g 
-nostdinc++ -o %t.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c %libcxx_includes -g 
-nostdinc++ -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error --libcxx --libc=uclibc  
%t.bc | FileCheck %s
 // Expect the following output:
diff --git a/test/CXX/symex/libc++/multi_throw.cpp 
b/test/CXX/symex/libc++/multi_throw.cpp
index 52e8d9b9..626585f4 100644
--- a/test/CXX/symex/libc++/multi_throw.cpp
+++ b/test/CXX/symex/libc++/multi_throw.cpp
@@ -2,7 +2,7 @@
 // Disabling msan because it times out on CI
 // REQUIRES: libcxx
 // REQUIRES: eh-cxx
-// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g 
-nostdinc++ -o %t1.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g 
-nostdinc++ -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | 
FileCheck %s
 
diff --git a/test/CXX/symex/libc++/multi_unwind.cpp 
b/test/CXX/symex/libc++/multi_unwind.cpp
index cf29422c..ab8d7a5c 100644
--- a/test/CXX/symex/libc++/multi_unwind.cpp
+++ b/test/CXX/symex/libc++/multi_unwind.cpp
@@ -2,7 +2,7 @@
 // Disabling msan because it times out on CI
 // REQUIRES: libcxx
 // REQUIRES: eh-cxx
-// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g 
-nostdinc++ -o %t1.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g 
-nostdinc++ -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | 
FileCheck %s
 
diff --git a/test/CXX/symex/libc++/nested.cpp b/test/CXX/symex/libc++/nested.cpp
index 21222642..1273a3b9 100644
--- a/test/CXX/symex/libc++/nested.cpp
+++ b/test/CXX/symex/libc++/nested.cpp
@@ -2,7 +2,7 @@
 // Disabling msan because it times out on CI
 // REQUIRES: libcxx
 // REQUIRES: eh-cxx
-// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g 
-nostdinc++ -o %t1.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g 
-nostdinc++ -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error --libc=uclibc --libcxx 
%t1.bc 2>&1 | FileCheck %s
 
diff --git a/test/CXX/symex/libc++/nested_fail.cpp 
b/test/CXX/symex/libc++/nested_fail.cpp
index d0b8ca09..4dce0279 100644
--- a/test/CXX/symex/libc++/nested_fail.cpp
+++ b/test/CXX/symex/libc++/nested_fail.cpp
@@ -2,7 +2,7 @@
 // Disabling msan because it times out on CI
 // REQUIRES: libcxx
 // REQUIRES: eh-cxx
-// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g 
-nostdinc++ -o %t1.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g 
-nostdinc++ -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | 
FileCheck %s
 
diff --git a/test/CXX/symex/libc++/rethrow.cpp 
b/test/CXX/symex/libc++/rethrow.cpp
index 149fe693..213cb1af 100644
--- a/test/CXX/symex/libc++/rethrow.cpp
+++ b/test/CXX/symex/libc++/rethrow.cpp
@@ -1,7 +1,7 @@
 // REQUIRES: uclibc
 // REQUIRES: libcxx
 // REQUIRES: eh-cxx
-// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c -I "%libcxx_include" -g 
-nostdinc++ -o %t.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c %libcxx_includes -g 
-nostdinc++ -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error --libcxx --libc=uclibc 
%t.bc 2>&1 | FileCheck %s
 
diff --git a/test/CXX/symex/libc++/simple_exception.cpp 
b/test/CXX/symex/libc++/simple_exception.cpp
index 0196e1eb..0ca8f8ed 100644
--- a/test/CXX/symex/libc++/simple_exception.cpp
+++ b/test/CXX/symex/libc++/simple_exception.cpp
@@ -2,7 +2,7 @@
 // Disabling msan because it times out on CI
 // REQUIRES: libcxx
 // REQUIRES: eh-cxx
-// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g 
-nostdinc++ -o %t1.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g 
-nostdinc++ -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | 
FileCheck %s
 
diff --git a/test/CXX/symex/libc++/simple_exception_fail.cpp 
b/test/CXX/symex/libc++/simple_exception_fail.cpp
index bda2cd33..793d9201 100644
--- a/test/CXX/symex/libc++/simple_exception_fail.cpp
+++ b/test/CXX/symex/libc++/simple_exception_fail.cpp
@@ -2,7 +2,7 @@
 // Disabling msan because it times out on CI
 // REQUIRES: libcxx
 // REQUIRES: eh-cxx
-// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g 
-nostdinc++ -o %t1.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g 
-nostdinc++ -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | 
FileCheck %s
 
diff --git a/test/CXX/symex/libc++/symbolic_exception.cpp 
b/test/CXX/symex/libc++/symbolic_exception.cpp
index 3f29fa04..50d682ba 100644
--- a/test/CXX/symex/libc++/symbolic_exception.cpp
+++ b/test/CXX/symex/libc++/symbolic_exception.cpp
@@ -2,7 +2,7 @@
 // Disabling msan because it times out on CI
 // REQUIRES: libcxx
 // REQUIRES: eh-cxx
-// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g 
-nostdinc++ -o %t1.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g 
-nostdinc++ -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | 
FileCheck %s
 
diff --git a/test/CXX/symex/libc++/throw_specifiers.cpp 
b/test/CXX/symex/libc++/throw_specifiers.cpp
index 96195cd4..efd6a0be 100644
--- a/test/CXX/symex/libc++/throw_specifiers.cpp
+++ b/test/CXX/symex/libc++/throw_specifiers.cpp
@@ -3,7 +3,7 @@
 // REQUIRES: uclibc
 // REQUIRES: libcxx
 // REQUIRES: eh-cxx
-// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c -I "%libcxx_include" -g 
-nostdinc++ -o %t.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -std=c++11 -c %libcxx_includes -g 
-nostdinc++ -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --libcxx --libc=uclibc  %t.bc | 
FileCheck %s
 
diff --git a/test/CXX/symex/libc++/throwing_exception_destructor.cpp 
b/test/CXX/symex/libc++/throwing_exception_destructor.cpp
index 02d7cdb9..7505027c 100644
--- a/test/CXX/symex/libc++/throwing_exception_destructor.cpp
+++ b/test/CXX/symex/libc++/throwing_exception_destructor.cpp
@@ -2,7 +2,7 @@
 // REQUIRES: uclibc
 // REQUIRES: libcxx
 // REQUIRES: eh-cxx
-// RUN: %clangxx %s -emit-llvm -O0 -std=c++11 -c -I "%libcxx_include" -g 
-nostdinc++ -o %t.bc
+// RUN: %clangxx %s -emit-llvm -O0 -std=c++11 -c %libcxx_includes -g 
-nostdinc++ -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --libcxx --libc=uclibc --exit-on-error  
%t.bc
 
diff --git a/test/CXX/symex/libc++/uncaught_exception.cpp 
b/test/CXX/symex/libc++/uncaught_exception.cpp
index 848013a0..4f9444a6 100644
--- a/test/CXX/symex/libc++/uncaught_exception.cpp
+++ b/test/CXX/symex/libc++/uncaught_exception.cpp
@@ -2,7 +2,7 @@
 // Disabling msan because it times out on CI
 // REQUIRES: libcxx
 // REQUIRES: eh-cxx
-// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g 
-nostdinc++ -o %t1.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g 
-nostdinc++ -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | 
FileCheck %s
 
diff --git a/test/CXX/symex/libc++/vector.cpp b/test/CXX/symex/libc++/vector.cpp
index 6f69ad65..33821b9e 100644
--- a/test/CXX/symex/libc++/vector.cpp
+++ b/test/CXX/symex/libc++/vector.cpp
@@ -2,7 +2,7 @@
 // Disabling msan because it times out on CI
 // REQUIRES: libcxx
 // REQUIRES: uclibc
-// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g 
-nostdinc++ -o %t1.bc
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g 
-nostdinc++ -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error --libc=uclibc --libcxx 
%t1.bc 2>&1 | FileCheck %s
 
diff --git a/test/lit.cfg b/test/lit.cfg
index cb47d3d4..c442c409 100644
--- a/test/lit.cfg
+++ b/test/lit.cfg
@@ -156,8 +156,11 @@ config.substitutions.append(
   ('%gentmp', os.path.join(klee_src_root, 'scripts/genTempFiles.sh'))
 )
 
+# Prepare the full include expression, i.e. for all given paths. For example, 
["path1","path2"]
+# becomes "-I path1 -I path2"
 config.substitutions.append(
-    ('%libcxx_include', getattr(config, 'libcxx_include_dir', None)))
+    ('%libcxx_includes', " ".join( ["-I "+ p for p in getattr(config, 
'libcxx_include_dirs', [])] ))
+    )
 
 # Add feature for the LLVM version in use, so it can be tested in REQUIRES and
 # XFAIL checks. We also add "not-XXX" variants, for the same reason.
diff --git a/test/lit.site.cfg.in b/test/lit.site.cfg.in
index c7063057..d185982b 100644
--- a/test/lit.site.cfg.in
+++ b/test/lit.site.cfg.in
@@ -9,7 +9,9 @@ config.klee_obj_root = "@KLEE_BINARY_DIR@"
 config.klee_tools_dir = "@KLEE_TOOLS_DIR@"
 config.llvm_tools_dir = "@LLVM_TOOLS_DIR@"
 
-config.libcxx_include_dir = "@KLEE_LIBCXX_INCLUDE_DIR@"
+config.libcxx_include_dirs = ["@KLEE_LIBCXX_INCLUDE_PATH@"]
+if len("@KLEE_LIBCXX_PLATFORM_INCLUDE_PATH@") > 0:
+    config.libcxx_include_dirs.append("@KLEE_LIBCXX_PLATFORM_INCLUDE_PATH@")
 
 # Needed to check if a hack needs to be applied
 config.llvm_version_major = "@LLVM_VERSION_MAJOR@"
-- 
2.43.0


++++++ 0004-Fix-klee-libc-memchr.c-compiler-warning.patch ++++++
From: Martin Nowack <m.now...@imperial.ac.uk>
Date: Thu, 12 Oct 2023 10:34:01 +0100
Subject: Fix `klee-libc/memchr.c` compiler warning
Patch-mainline: no
References: llvm16

Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 runtime/klee-libc/memchr.c | 23 +++++++++--------------
 1 file changed, 9 insertions(+), 14 deletions(-)

diff --git a/runtime/klee-libc/memchr.c b/runtime/klee-libc/memchr.c
index fe0670a7..3cd47cdf 100644
--- a/runtime/klee-libc/memchr.c
+++ b/runtime/klee-libc/memchr.c
@@ -36,19 +36,14 @@
 
 #include <string.h>
 
-void *
-memchr(s, c, n)
-       const void *s;
-       int c;
-       size_t n;
-{
-       if (n != 0) {
-               const unsigned char *p = s;
+void *memchr(const void *s, int c, size_t n) {
+  if (n != 0) {
+    const unsigned char *p = s;
 
-               do {
-                       if (*p++ == c)
-                               return ((void *)(p - 1));
-               } while (--n != 0);
-       }
-       return (NULL);
+    do {
+      if (*p++ == c)
+        return ((void *)(p - 1));
+    } while (--n != 0);
+  }
+  return (NULL);
 }
-- 
2.43.0


++++++ 0005-Fix-klee_eh_cxx.cpp-compiler-error.patch ++++++
From: Martin Nowack <m.now...@imperial.ac.uk>
Date: Thu, 12 Oct 2023 10:34:33 +0100
Subject: Fix `klee_eh_cxx.cpp` compiler error
Patch-mainline: no
References: llvm16

Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 runtime/klee-eh-cxx/klee_eh_cxx.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/runtime/klee-eh-cxx/klee_eh_cxx.cpp 
b/runtime/klee-eh-cxx/klee_eh_cxx.cpp
index 9d86bef4..cb5e0c7c 100644
--- a/runtime/klee-eh-cxx/klee_eh_cxx.cpp
+++ b/runtime/klee-eh-cxx/klee_eh_cxx.cpp
@@ -90,7 +90,7 @@ get_thrown_object_ptr(_Unwind_Exception* unwind_exception)
 // Our implementation of a personality function for handling
 // libcxxabi-exceptions. Follows how libcxxabi's __gxx_personality_v0 handles
 // exceptions.
-[[gnu::used]] extern "C" std::int32_t
+extern "C" std::int32_t
 _klee_eh_cxx_personality(_Unwind_Exception *exceptionPointer,
                          const std::size_t num_bytes,
                          const unsigned char *lp_clauses) {
-- 
2.43.0


++++++ 0006-Refactor-invocation-of-old-pass-manager-into-legacy-.patch ++++++
++++ 1002 lines (skipped)

++++++ 0007-Use-KLEE-s-uClibc-v1.4-as-default-to-support-the-com.patch ++++++
From: Martin Nowack <m.now...@imperial.ac.uk>
Date: Sun, 29 Oct 2023 20:38:55 +0000
Subject: Use KLEE's uClibc v1.4 as default to support the compilation with
 newer compilers
Patch-mainline: no
References: llvm16

Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 .github/workflows/build.yaml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml
index 96122bcb..fa924a37 100644
--- a/.github/workflows/build.yaml
+++ b/.github/workflows/build.yaml
@@ -24,7 +24,7 @@ env:
   SOLVERS: STP:Z3
   STP_VERSION: 2.3.3
   TCMALLOC_VERSION: 2.9.1
-  UCLIBC_VERSION: klee_uclibc_v1.3
+  UCLIBC_VERSION: klee_uclibc_v1.4
   USE_TCMALLOC: 1
   USE_LIBCXX: 1
   Z3_VERSION: 4.8.15
-- 
2.43.0


++++++ 0008-Assume-C-compiler-s-default-standard-is-std-gnu17.patch ++++++
++++ 1159 lines (skipped)

++++++ 0009-Explicitly-build-KLEE-s-exception-handling-runtime-w.patch ++++++
From: Martin Nowack <m.now...@imperial.ac.uk>
Date: Mon, 30 Oct 2023 12:03:22 +0000
Subject: Explicitly build KLEE's exception handling runtime with C++11
Patch-mainline: no
References: llvm16

Currently, we assume C++11 support being used to by the tested software.
This needs to change if newer C++ standards should be supported.

Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 runtime/klee-eh-cxx/CMakeLists.txt | 1 +
 1 file changed, 1 insertion(+)

diff --git a/runtime/klee-eh-cxx/CMakeLists.txt 
b/runtime/klee-eh-cxx/CMakeLists.txt
index 470e3f0a..b51b8544 100644
--- a/runtime/klee-eh-cxx/CMakeLists.txt
+++ b/runtime/klee-eh-cxx/CMakeLists.txt
@@ -17,6 +17,7 @@ set(ADDITIONAL_CXX_FLAGS
         -I "${KLEE_LIBCXXABI_SRC_DIR}/src"
         -I "${KLEE_LIBCXXABI_SRC_DIR}/include"
         -I "${KLEE_LIBCXX_INCLUDE_PATH}"
+        -std=c++11
 )
 
 if (KLEE_LIBCXX_PLATFORM_INCLUDE_PATH)
-- 
2.43.0


++++++ 0010-Explicitly-enable-opaque-pointer-support-for-LLVM-15.patch ++++++
From: Martin Nowack <m.now...@imperial.ac.uk>
Date: Mon, 30 Oct 2023 14:26:01 +0000
Subject: Explicitly enable opaque pointer support for LLVM 15
Patch-mainline: no
References: llvm16

This automatically lifts old-style pointers to opaque pointerws.
More recent versions use opaque pointers automatically and do not need
an explicit enabling.

Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 test/Concrete/Makefile.cmake.test.in | 6 ++++--
 tools/klee/main.cpp                  | 4 ++++
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/test/Concrete/Makefile.cmake.test.in 
b/test/Concrete/Makefile.cmake.test.in
index 2282bb08..765ea690 100644
--- a/test/Concrete/Makefile.cmake.test.in
+++ b/test/Concrete/Makefile.cmake.test.in
@@ -14,6 +14,8 @@ LLVMCC := @LLVMCC@
 LLVMAS := @LLVM_AS@
 LLVMLINK := @LLVM_LINK@
 LLVMCC.CFlags := @OZERO_OPT@ -Wall
+LLVMAS.Flags := @LLVM_AS_FLAGS@
+LLVMLINK.Flags := @LLVM_LINK_FLAGS@
 
 # Make sure source files can match the pattern rules
 VPATH := @CMAKE_CURRENT_SOURCE_DIR@
@@ -28,7 +30,7 @@ Output/%.bc: %.c Output/.dir
        $(LLVMCC) -emit-llvm -c $(LLVMCC.CFlags) $< -o $@
 
 Output/%.bc: %.ll $(LLVMAS) Output/.dir
-       $(LLVMAS) -f $< -o $@
+       $(LLVMAS) $(LLVMAS.Flags) -f $< -o $@
 
 # We build a separate testingUtils bitcode for each test, to make sure parallel
 # tests don't interact with one another.
@@ -36,7 +38,7 @@ Output/%_testingUtils.bc: _testingUtils.c Output/.dir
        $(LLVMCC) -emit-llvm -c $(LLVMCC.CFlags) $< -o $@
 
 Output/linked_%.bc: Output/%.bc Output/%_testingUtils.bc
-       $(LLVMLINK) $< Output/$*_testingUtils.bc -o $@
+       $(LLVMLINK) $(LLVMLINK.Flags) $< Output/$*_testingUtils.bc -o $@
 
 .PRECIOUS: Output/.dir
 
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index a3062d24..340daf0b 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -1202,6 +1202,10 @@ int main(int argc, char **argv, char **envp) {
   // Load the bytecode...
   std::string errorMsg;
   LLVMContext ctx;
+#if LLVM_VERSION_CODE == LLVM_VERSION(15, 0)
+  // We have to force the upgrade to opaque pointer explicitly for LLVM 15.
+  ctx.setOpaquePointers(true);
+#endif
   std::vector<std::unique_ptr<llvm::Module>> loadedModules;
   if (!klee::loadFile(InputFile, ctx, loadedModules, errorMsg)) {
     klee_error("error loading program '%s': %s", InputFile.c_str(),
-- 
2.43.0


++++++ 0011-Add-support-for-opaque-pointers.patch ++++++
From: Martin Nowack <m.now...@imperial.ac.uk>
Date: Mon, 30 Oct 2023 14:46:22 +0000
Subject: Add support for opaque pointers
Patch-mainline: no
References: llvm16

Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 lib/Core/Executor.cpp                | 119 ++++++++++++++++++++++-----
 lib/Core/ExternalDispatcher.cpp      |  20 ++++-
 lib/Core/GetElementPtrTypeIterator.h |   8 --
 lib/Module/FunctionAlias.cpp         |   8 +-
 lib/Module/IntrinsicCleaner.cpp      |  11 ++-
 5 files changed, 132 insertions(+), 34 deletions(-)

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index b4da6a08..58c15141 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -14,7 +14,9 @@
 #include "CoreStats.h"
 #include "ExecutionState.h"
 #include "ExternalDispatcher.h"
+#if LLVM_VERSION_CODE <= LLVM_VERSION(14, 0)
 #include "GetElementPtrTypeIterator.h"
+#endif
 #include "ImpliedValue.h"
 #include "Memory.h"
 #include "MemoryManager.h"
@@ -67,6 +69,9 @@
 #include "llvm/IR/LLVMContext.h"
 #include "llvm/IR/Module.h"
 #include "llvm/IR/Operator.h"
+#if LLVM_VERSION_CODE >= LLVM_VERSION(15, 0)
+#include "llvm/IR/GetElementPtrTypeIterator.h"
+#endif
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/ErrorHandling.h"
 #include "llvm/Support/FileSystem.h"
@@ -1464,24 +1469,25 @@ MemoryObject 
*Executor::serializeLandingpad(ExecutionState &state,
   stateTerminated = false;
 
   std::vector<unsigned char> serialized;
-
   for (unsigned current_clause_id = 0; current_clause_id < lpi.getNumClauses();
        ++current_clause_id) {
-    llvm::Constant *current_clause = lpi.getClause(current_clause_id);
     if (lpi.isCatch(current_clause_id)) {
       // catch-clause
       serialized.push_back(0);
 
       std::uint64_t ti_addr = 0;
 
-      llvm::BitCastOperator *clause_bitcast =
-          dyn_cast<llvm::BitCastOperator>(current_clause);
-      if (clause_bitcast) {
-        llvm::GlobalValue *clause_type =
+      llvm::Constant *catchClause = lpi.getClause(current_clause_id);
+      llvm::Constant *typeInfo = catchClause->stripPointerCasts();
+      if (auto *gv = dyn_cast<llvm::GlobalVariable>(typeInfo)) {
+        ti_addr = globalAddresses[gv]->getZExtValue();
+      } else if (auto *clause_bitcast =
+                     dyn_cast<llvm::BitCastOperator>(catchClause)) {
+        auto *clause_type =
             dyn_cast<GlobalValue>(clause_bitcast->getOperand(0));
 
         ti_addr = globalAddresses[clause_type]->getZExtValue();
-      } else if (current_clause->isNullValue()) {
+      } else if (catchClause->isNullValue()) {
         ti_addr = 0;
       } else {
         terminateStateOnExecError(
@@ -1493,15 +1499,16 @@ MemoryObject 
*Executor::serializeLandingpad(ExecutionState &state,
       serialized.resize(old_size + 8);
       memcpy(serialized.data() + old_size, &ti_addr, sizeof(ti_addr));
     } else if (lpi.isFilter(current_clause_id)) {
-      if (current_clause->isNullValue()) {
+      llvm::Constant *filter_clause = lpi.getClause(current_clause_id);
+
+      if (filter_clause->isNullValue()) {
         // special handling for a catch-all filter clause, i.e., "[0 x i8*]"
         // for this case we serialize 1 element..
         serialized.push_back(1);
         // which is a 64bit-wide 0.
         serialized.resize(serialized.size() + 8, 0);
       } else {
-        llvm::ConstantArray const *ca =
-            cast<llvm::ConstantArray>(current_clause);
+        const auto *ca = cast<llvm::ConstantArray>(filter_clause);
 
         // serialize `num_elements+1` as unsigned char
         unsigned const num_elements = ca->getNumOperands();
@@ -1520,18 +1527,16 @@ MemoryObject 
*Executor::serializeLandingpad(ExecutionState &state,
 
         // serialize the exception-types occurring in this filter-clause
         for (llvm::Value const *v : ca->operands()) {
-          llvm::BitCastOperator const *bitcast =
-              dyn_cast<llvm::BitCastOperator>(v);
-          if (!bitcast) {
-            terminateStateOnExecError(state,
-                                      "Internal: expected value inside a "
-                                      "filter-clause to be a bitcast");
-            stateTerminated = true;
-            return nullptr;
+          llvm::GlobalValue const *clause_value = nullptr;
+
+          if (auto const *bitcast = dyn_cast<llvm::BitCastOperator>(v)) {
+            clause_value = dyn_cast<GlobalValue>(bitcast->getOperand(0));
+          }
+
+          if (auto *gv = dyn_cast<llvm::GlobalVariable>(v)) {
+            clause_value = gv;
           }
 
-          llvm::GlobalValue const *clause_value =
-              dyn_cast<GlobalValue>(bitcast->getOperand(0));
           if (!clause_value) {
             terminateStateOnExecError(state,
                                       "Internal: expected value inside a "
@@ -2150,7 +2155,7 @@ void Executor::executeInstruction(ExecutionState &state, 
KInstruction *ki) {
           unwindToNextLandingpad(state);
         } else {
           // a clause (or a catch-all clause or filter clause) matches:
-          // remember the stack index and switch to cleanup phase
+          // remember the stack index and switch to clean-up phase
           state.unwindingInformation =
               std::make_unique<CleanupPhaseUnwindingInformation>(
                   sui->exceptionObject, cast<ConstantExpr>(result),
@@ -2457,8 +2462,12 @@ void Executor::executeInstruction(ExecutionState &state, 
KInstruction *ki) {
 
     if (f) {
       const FunctionType *fType = f->getFunctionType();
+#if LLVM_VERSION_MAJOR >= 15
+      const FunctionType *fpType = cb.getFunctionType();
+#else
       const FunctionType *fpType =
           dyn_cast<FunctionType>(fp->getType()->getPointerElementType());
+#endif
 
       // special case the call with a bitcast case
       if (fType != fpType) {
@@ -3365,10 +3374,17 @@ template <typename TypeIt>
 void Executor::computeOffsetsSeqTy(KGEPInstruction *kgepi,
                                    ref<ConstantExpr> &constantOffset,
                                    uint64_t index, const TypeIt it) {
+#if LLVM_VERSION_CODE <= LLVM_VERSION(14, 0)
   assert(it->getNumContainedTypes() == 1 &&
          "Sequential type must contain one subtype");
   uint64_t elementSize =
       kmodule->targetData->getTypeStoreSize(it->getContainedType(0));
+#else
+  assert(it.isSequential() && "Called with non-sequential type");
+  // Get the size of a single element
+  uint64_t elementSize =
+      kmodule->targetData->getTypeStoreSize(it.getIndexedType());
+#endif
   const Value *operand = it.getOperand();
   if (const Constant *c = dyn_cast<Constant>(operand)) {
     ref<ConstantExpr> index =
@@ -3387,13 +3403,21 @@ void Executor::computeOffsets(KGEPInstruction *kgepi, 
TypeIt ib, TypeIt ie) {
     ConstantExpr::alloc(0, Context::get().getPointerWidth());
   uint64_t index = 1;
   for (TypeIt ii = ib; ii != ie; ++ii) {
+#if LLVM_VERSION_CODE <= LLVM_VERSION(14, 0)
     if (StructType *st = dyn_cast<StructType>(*ii)) {
+#else
+    if (StructType *st = ii.getStructTypeOrNull()) {
+#endif
       const StructLayout *sl = kmodule->targetData->getStructLayout(st);
       const ConstantInt *ci = cast<ConstantInt>(ii.getOperand());
       uint64_t addend = sl->getElementOffset((unsigned) ci->getZExtValue());
       constantOffset = constantOffset->Add(ConstantExpr::alloc(addend,
                                                                
Context::get().getPointerWidth()));
+#if LLVM_VERSION_CODE <= LLVM_VERSION(14, 0)
     } else if (ii->isArrayTy() || ii->isVectorTy() || ii->isPointerTy()) {
+#else
+    } else if (ii.isSequential()) {
+#endif
       computeOffsetsSeqTy(kgepi, constantOffset, index, ii);
     } else
       assert("invalid type" && 0);
@@ -3405,15 +3429,66 @@ void Executor::computeOffsets(KGEPInstruction *kgepi, 
TypeIt ib, TypeIt ie) {
 void Executor::bindInstructionConstants(KInstruction *KI) {
   if (GetElementPtrInst *gepi = dyn_cast<GetElementPtrInst>(KI->inst)) {
     KGEPInstruction *kgepi = static_cast<KGEPInstruction *>(KI);
-    computeOffsets(kgepi, gep_type_begin(gepi), gep_type_end(gepi));
+#if LLVM_VERSION_CODE <= LLVM_VERSION(14, 0)
+    computeOffsets(kgepi, klee::gep_type_begin(gepi), 
klee::gep_type_end(gepi));
+#else
+    computeOffsets(kgepi, llvm::gep_type_begin(gepi), 
llvm::gep_type_end(gepi));
+#endif
   } else if (InsertValueInst *ivi = dyn_cast<InsertValueInst>(KI->inst)) {
     KGEPInstruction *kgepi = static_cast<KGEPInstruction *>(KI);
+#if LLVM_VERSION_CODE <= LLVM_VERSION(10, 0)
     computeOffsets(kgepi, iv_type_begin(ivi), iv_type_end(ivi));
     assert(kgepi->indices.empty() && "InsertValue constant offset expected");
+#else
+    llvm::Value *agg = ivi->getAggregateOperand();
+    llvm::Type *current_type = agg->getType();
+    uint64_t offset = 0;
+    for (auto index : ivi->indices()) {
+      if (StructType *st = dyn_cast<llvm::StructType>(current_type)) {
+        const StructLayout *sl = kmodule->targetData->getStructLayout(st);
+        uint64_t addend = sl->getElementOffset(index);
+        offset = offset + addend;
+      } else if (current_type->isArrayTy() || current_type->isVectorTy() ||
+                 current_type->isPointerTy()) {
+        uint64_t elementSize = kmodule->targetData->getTypeStoreSize(
+            current_type->getArrayElementType());
+        offset += elementSize * index;
+      } else {
+        assert(0 && "Unknown type");
+      }
+
+      current_type = GetElementPtrInst::getTypeAtIndex(current_type, index);
+    }
+    kgepi->offset = offset;
+#endif
   } else if (ExtractValueInst *evi = dyn_cast<ExtractValueInst>(KI->inst)) {
     KGEPInstruction *kgepi = static_cast<KGEPInstruction *>(KI);
+#if LLVM_VERSION_CODE <= LLVM_VERSION(10, 0)
     computeOffsets(kgepi, ev_type_begin(evi), ev_type_end(evi));
     assert(kgepi->indices.empty() && "ExtractValue constant offset expected");
+#else
+
+    llvm::Value *agg = evi->getAggregateOperand();
+    llvm::Type *current_type = agg->getType();
+    uint64_t offset = 0;
+    for (auto index : evi->indices()) {
+      if (StructType *st = dyn_cast<llvm::StructType>(current_type)) {
+        const StructLayout *sl = kmodule->targetData->getStructLayout(st);
+        uint64_t addend = sl->getElementOffset(index);
+        offset = offset + addend;
+      } else if (current_type->isArrayTy() || current_type->isVectorTy() ||
+                 current_type->isPointerTy()) {
+        uint64_t elementSize = kmodule->targetData->getTypeStoreSize(
+            current_type->getArrayElementType());
+        offset += elementSize * index;
+      } else {
+        assert(0 && "Unknown type");
+      }
+
+      current_type = GetElementPtrInst::getTypeAtIndex(current_type, index);
+    }
+    kgepi->offset = offset;
+#endif
   }
 }
 
diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp
index 718b1c31..7b43218b 100644
--- a/lib/Core/ExternalDispatcher.cpp
+++ b/lib/Core/ExternalDispatcher.cpp
@@ -250,7 +250,7 @@ bool ExternalDispatcherImpl::runProtectedCall(Function *f, 
uint64_t *args) {
 }
 
 // FIXME: This might have been relevant for the old JIT but the MCJIT
-// has a completly different implementation so this comment below is
+// has a completely different implementation so this comment below is
 // likely irrelevant and misleading.
 //
 // For performance purposes we construct the stub in such a way that the
@@ -283,13 +283,20 @@ Function 
*ExternalDispatcherImpl::createDispatcher(KCallable *target,
 
   llvm::IRBuilder<> Builder(dBB);
   // Get a Value* for &gTheArgsP, as an i64**.
+#if LLVM_VERSION_CODE >= LLVM_VERSION(15, 0)
+  auto argI64sp = Builder.CreateIntToPtr(
+      ConstantInt::get(Type::getInt64Ty(ctx), (uintptr_t)&gTheArgsP),
+      PointerType::getUnqual(PointerType::getUnqual(Type::getInt64Ty(ctx))),
+      "argsp");
+  auto argI64s = Builder.CreateLoad(Builder.getPtrTy(), argI64sp, "args");
+#else
   auto argI64sp = Builder.CreateIntToPtr(
       ConstantInt::get(Type::getInt64Ty(ctx), (uintptr_t)(void *)&gTheArgsP),
       PointerType::getUnqual(PointerType::getUnqual(Type::getInt64Ty(ctx))),
       "argsp");
   auto argI64s = Builder.CreateLoad(
       argI64sp->getType()->getPointerElementType(), argI64sp, "args");
-
+#endif
   // Get the target function type.
   FunctionType *FTy = target->getFunctionType();
 
@@ -306,6 +313,14 @@ Function 
*ExternalDispatcherImpl::createDispatcher(KCallable *target,
     if (argTy->isX86_FP80Ty() && idx & 0x01)
       idx++;
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(15, 0)
+    auto argI64p =
+        Builder.CreateGEP(Builder.getPtrTy(), argI64s,
+                          ConstantInt::get(Type::getInt32Ty(ctx), idx));
+
+    auto argp = Builder.CreateBitCast(argI64p, PointerType::getUnqual(argTy));
+    args[i] = Builder.CreateLoad(argTy, argp);
+#else
     auto argI64p =
         Builder.CreateGEP(argI64s->getType()->getPointerElementType(), argI64s,
                           ConstantInt::get(Type::getInt32Ty(ctx), idx));
@@ -313,6 +328,7 @@ Function 
*ExternalDispatcherImpl::createDispatcher(KCallable *target,
     auto argp = Builder.CreateBitCast(argI64p, PointerType::getUnqual(argTy));
     args[i] =
         Builder.CreateLoad(argp->getType()->getPointerElementType(), argp);
+#endif
 
     unsigned argSize = argTy->getPrimitiveSizeInBits();
     idx += ((!!argSize ? argSize : 64) + 63) / 64;
diff --git a/lib/Core/GetElementPtrTypeIterator.h 
b/lib/Core/GetElementPtrTypeIterator.h
index d8b0e097..4e0314cb 100644
--- a/lib/Core/GetElementPtrTypeIterator.h
+++ b/lib/Core/GetElementPtrTypeIterator.h
@@ -144,14 +144,6 @@ public:
     return iv_type_iterator::end(IV->idx_end());
   }
 
-  inline vce_type_iterator vce_type_begin(const llvm::ConstantExpr *CE) {
-    return vce_type_iterator::begin(CE->getOperand(0)->getType(),
-                                    CE->getIndices().begin());
-  }
-  inline vce_type_iterator vce_type_end(const llvm::ConstantExpr *CE) {
-    return vce_type_iterator::end(CE->getIndices().end());
-  }
-
   template <typename ItTy>
   inline generic_gep_type_iterator<ItTy> gep_type_begin(llvm::Type *Op0, ItTy 
I,
                                                         ItTy E) {
diff --git a/lib/Module/FunctionAlias.cpp b/lib/Module/FunctionAlias.cpp
index aa80b35d..c00bde58 100644
--- a/lib/Module/FunctionAlias.cpp
+++ b/lib/Module/FunctionAlias.cpp
@@ -134,10 +134,16 @@ bool FunctionAliasPass::runOnModule(Module &M) {
 }
 
 const FunctionType *FunctionAliasPass::getFunctionType(const GlobalValue *gv) {
+#if LLVM_VERSION_CODE >= LLVM_VERSION(15, 0)
+  if (auto *ft = dyn_cast<FunctionType>(gv->getType()))
+    return ft;
+  return dyn_cast<FunctionType>(gv->getValueType());
+#else
   const Type *type = gv->getType();
   while (type->isPointerTy())
     type = type->getPointerElementType();
-  return cast<FunctionType>(type);
+  return dyn_cast<FunctionType>(type);
+#endif
 }
 
 bool FunctionAliasPass::checkType(const GlobalValue *match,
diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp
index ad7c0631..40ff2874 100644
--- a/lib/Module/IntrinsicCleaner.cpp
+++ b/lib/Module/IntrinsicCleaner.cpp
@@ -100,9 +100,14 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, 
Module &M) {
               Builder.CreatePointerCast(dst, i8pp, "vacopy.cast.dst");
           auto castedSrc =
               Builder.CreatePointerCast(src, i8pp, "vacopy.cast.src");
+#if LLVM_VERSION_CODE >= LLVM_VERSION(15, 0)
+          auto load = Builder.CreateLoad(Builder.getInt8PtrTy(), castedSrc,
+                                         "vacopy.read");
+#else
           auto load =
               Builder.CreateLoad(castedSrc->getType()->getPointerElementType(),
                                  castedSrc, "vacopy.read");
+#endif
           Builder.CreateStore(load, castedDst, false /* isVolatile */);
         } else {
           assert(WordSize == 8 && "Invalid word size!");
@@ -110,9 +115,13 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, 
Module &M) {
           auto pDst = Builder.CreatePointerCast(dst, i64p, "vacopy.cast.dst");
           auto pSrc = Builder.CreatePointerCast(src, i64p, "vacopy.cast.src");
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(15, 0)
+          auto pSrcType = Builder.getPtrTy();
+          auto pDstType = Builder.getPtrTy();
+#else
           auto pSrcType = pSrc->getType()->getPointerElementType();
           auto pDstType = pDst->getType()->getPointerElementType();
-
+#endif
           auto val = Builder.CreateLoad(pSrcType, pSrc);
           Builder.CreateStore(val, pDst, ii);
 
-- 
2.43.0


++++++ 0012-Fix-test-cases-to-support-opaque-pointers.patch ++++++
From: Martin Nowack <m.now...@imperial.ac.uk>
Date: Mon, 30 Oct 2023 14:48:58 +0000
Subject: Fix test cases to support opaque pointers
Patch-mainline: no
References: llvm16

Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 test/CXX/LandingPad.cpp       |   2 +
 test/Concrete/CMakeLists.txt  |   4 ++
 test/Feature/KleeStats.c      |   2 +-
 test/Feature/VarArgByVal.c    |   8 +--
 test/Feature/VarArgByValOld.c | 131 ++++++++++++++++++++++++++++++++++
 test/Feature/asm_lifting.ll   |   2 +-
 6 files changed, 143 insertions(+), 6 deletions(-)
 create mode 100644 test/Feature/VarArgByValOld.c

diff --git a/test/CXX/LandingPad.cpp b/test/CXX/LandingPad.cpp
index 18cad7c8..6b6e6748 100644
--- a/test/CXX/LandingPad.cpp
+++ b/test/CXX/LandingPad.cpp
@@ -1,3 +1,5 @@
+// REQUIRES: lt-llvm-15.0
+// Different LLVM IR syntax with opaque ptr - it's a nullptr directly, no 
constant
 // RUN: %clangxx %s -emit-llvm -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s
diff --git a/test/Concrete/CMakeLists.txt b/test/Concrete/CMakeLists.txt
index e7cf2416..a073482c 100644
--- a/test/Concrete/CMakeLists.txt
+++ b/test/Concrete/CMakeLists.txt
@@ -8,4 +8,8 @@
 
#===------------------------------------------------------------------------===#
 
 set(OZERO_OPT "-O0 -Xclang -disable-O0-optnone")
+if ("${LLVM_VERSION_MAJOR}" EQUAL 15)
+    set(LLVM_AS_FLAGS "-opaque-pointers")
+    set(LLVM_LINK_FLAGS "-opaque-pointers")
+endif ()
 configure_file(Makefile.cmake.test.in Makefile.cmake.test @ONLY)
diff --git a/test/Feature/KleeStats.c b/test/Feature/KleeStats.c
index 2a498beb..8045f22e 100644
--- a/test/Feature/KleeStats.c
+++ b/test/Feature/KleeStats.c
@@ -29,7 +29,7 @@ int main(){
 // First check we find a line with the expected format
 // CHECK-STATS: 
Path,Instrs,Time(s),ICov(%),BCov(%),ICount,TSolver(%),ActiveStates,MaxActiveStates,Mem(MiB),MaxMem(MiB)
 // Check there is a line with .klee-out dir, non zero instruction, less than 1 
second execution time and 100 ICov.
-// CHECK-STATS: {{.*\.klee-out,[1-9]+,[0-9]+\.([0-9]+),100\.00}}
+// CHECK-STATS: {{.*\.klee-out,[1-9][0-9]+,[0-9]+\.([0-9]+),100\.00}}
 
 // Check other formats
 // CHECK-STATS-ABS-TIMES: 
Path,Time(s),TUser(s),TResolve(s),TCex(s),TSolver(s),TFork(s)
diff --git a/test/Feature/VarArgByVal.c b/test/Feature/VarArgByVal.c
index 551e6c63..7b979f61 100644
--- a/test/Feature/VarArgByVal.c
+++ b/test/Feature/VarArgByVal.c
@@ -1,4 +1,5 @@
-/* This test checks that KLEE correctly handles variadic arguments with the 
+// REQUIRES: geq-llvm-15.0
+/* This test checks that KLEE correctly handles variadic arguments with the
    byval attribute */
 
 // RUN: %clang %s -emit-llvm %O0opt -c -g -o %t1.bc
@@ -7,9 +8,8 @@
 // RUN: FileCheck %s --input-file=%t.klee-out/assembly.ll
 //
 // TODO: Make noundef unconditional when LLVM 14 is the oldest supported 
version.
-// CHECK: @test1({{.*}}, i32 {{(noundef )?}}-1, %struct.foo* {{(noundef 
)?}}byval{{.*}} %struct.bar* {{(noundef )?}}byval
-// CHECK: @test2({{.*}}, %struct.foo* {{(noundef )?}}byval{{.*}} %struct.bar* 
{{(noundef )?}}byval
-
+// CHECK: call void (ptr, i32, ...) @test1(ptr sret(%struct.foo) align 8 
{{.*}}, i32 noundef -1, ptr noundef byval(%struct.foo) align 8 {{.*}}, ptr 
noundef byval(%struct.bar) align 8 {{.*}})
+// CHECK: call void (ptr, i32, i64, ...) @test2(ptr sret(%struct.foo) align 8 
%tmp, i32 noundef {{.*}}, i64 noundef {{.*}}, i32 noundef {{.*}}, ptr noundef 
byval(%struct.foo) align 8 {{.*}}, i64 noundef {{.*}}, ptr noundef 
byval(%struct.bar) align 8 {{.*}}, ptr noundef byval(%struct.foo) align 8 
{{.*}}, ptr noundef byval(%struct.bar) align 8 {{.*}})
 #include <stdarg.h>
 #include <assert.h>
 #include <stdio.h>
diff --git a/test/Feature/VarArgByValOld.c b/test/Feature/VarArgByValOld.c
new file mode 100644
index 00000000..011046d8
--- /dev/null
+++ b/test/Feature/VarArgByValOld.c
@@ -0,0 +1,131 @@
+// REQUIRES: lt-llvm-15.0
+/* This test checks that KLEE correctly handles variadic arguments with the
+   byval attribute */
+
+// RUN: %clang %s -emit-llvm %O0opt -c -g -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --exit-on-error --output-dir=%t.klee-out %t1.bc
+// RUN: FileCheck %s --input-file=%t.klee-out/assembly.ll
+//
+// TODO: Make noundef unconditional when LLVM 14 is the oldest supported 
version.
+// CHECK: @test1({{.*}}, i32 {{(noundef )?}}-1, %struct.foo* {{(noundef 
)?}}byval{{.*}} %struct.bar* {{(noundef )?}}byval
+// CHECK: @test2({{.*}}, %struct.foo* {{(noundef )?}}byval{{.*}} %struct.bar* 
{{(noundef )?}}byval
+#include <assert.h>
+#include <stdarg.h>
+#include <stdio.h>
+
+struct foo {
+  char f1;
+  long long f2;
+  long long f3;
+  char f4;
+  long f5;
+  int f6;
+  char f7;
+};
+
+struct bar {
+  long long int f1;
+  char f2;
+  long long f3;
+  char f4;
+  long f5;
+};
+
+struct foo test1(int x, ...) {
+  va_list ap;
+  va_start(ap, x);
+  assert(x == -1);
+
+  struct foo f = va_arg(ap, struct foo);
+  assert(f.f1 == 1);
+  assert(f.f2 == 2);
+  assert(f.f3 == 3);
+  assert(f.f4 == 4);
+  assert(f.f5 == 5);
+  assert(f.f6 == 6);
+  assert(f.f7 == 7);
+
+  struct bar b = va_arg(ap, struct bar);
+  assert(b.f1 == 11);
+  assert(b.f2 == 12);
+  assert(b.f3 == 13);
+  assert(b.f4 == 14);
+  assert(b.f5 == 15);
+
+  va_end(ap);
+
+  f.f1++;
+  return f;
+}
+
+struct foo test2(int x, long long int l, ...) {
+  va_list ap;
+  va_start(ap, l);
+  assert(x == 10);
+  assert(l == 1000);
+
+  int i = va_arg(ap, int);
+  assert(i == 10);
+
+  struct foo f = va_arg(ap, struct foo);
+  assert(f.f1 == 1);
+  assert(f.f2 == 2);
+  assert(f.f3 == 3);
+  assert(f.f4 == 4);
+  assert(f.f5 == 5);
+  assert(f.f6 == 6);
+  assert(f.f7 == 7);
+
+  l = va_arg(ap, long long int);
+  assert(l == 1000);
+
+  struct bar b = va_arg(ap, struct bar);
+  assert(b.f1 == 11);
+  assert(b.f2 == 12);
+  assert(b.f3 == 13);
+  assert(b.f4 == 14);
+  assert(b.f5 == 15);
+
+  f = va_arg(ap, struct foo);
+  assert(f.f1 == 10);
+  assert(f.f2 == 20);
+  assert(f.f3 == 30);
+  assert(f.f4 == 40);
+  assert(f.f5 == 50);
+  assert(f.f6 == 60);
+  assert(f.f7 == 70);
+
+  b = va_arg(ap, struct bar);
+  assert(b.f1 == 1);
+  assert(b.f2 == 3);
+  assert(b.f3 == 5);
+  assert(b.f4 == 7);
+  assert(b.f5 == 9);
+
+  va_end(ap);
+
+  f.f1++;
+  return f;
+}
+
+int main() {
+  struct foo f = {1, 2, 3, 4, 5, 6, 7};
+  struct bar b = {11, 12, 13, 14, 15};
+  struct foo res = test1(-1, f, b);
+  assert(res.f1 == 2);
+  assert(res.f2 == 2);
+  assert(res.f3 == 3);
+  assert(res.f4 == 4);
+  assert(res.f5 == 5);
+  assert(res.f6 == 6);
+  assert(res.f7 == 7);
+  // check that f was not modified, as it's passed by value
+  assert(f.f1 == 1);
+
+  int i = 10;
+  long long int l = 1000;
+  struct foo f2 = {10, 20, 30, 40, 50, 60, 70};
+  struct bar b2 = {1, 3, 5, 7, 9};
+  test2(i, l, i, f, l, b, f2, b2);
+}
diff --git a/test/Feature/asm_lifting.ll b/test/Feature/asm_lifting.ll
index d99db0cf..115bc2f9 100644
--- a/test/Feature/asm_lifting.ll
+++ b/test/Feature/asm_lifting.ll
@@ -17,7 +17,7 @@ entry:
   %1 = getelementptr inbounds [47 x i8], [47 x i8]* %0, i64 0, i64 0
   ; Make sure memory barrier with function arguments is kept
   %2 = call i8* asm sideeffect "", 
"=r,0,~{memory},~{dirflag},~{fpsr},~{flags}"(i8* nonnull %1)
-  ; CHECK: %2 = call i8* asm sideeffect "", 
"=r,0,~{memory},~{dirflag},~{fpsr},~{flags}"(i8* nonnull %1)
+  ; CHECK: %2 = call {{.*}} asm sideeffect "", 
"=r,0,~{memory},~{dirflag},~{fpsr},~{flags}"({{.*}} nonnull %1)
   ret i32 0
 }
 
-- 
2.43.0


++++++ 0013-Fix-test-case-using-unsupported-CHECK_NEXT-instead-o.patch ++++++
From: Martin Nowack <m.now...@imperial.ac.uk>
Date: Mon, 30 Oct 2023 14:50:51 +0000
Subject: Fix test case: using unsupported `CHECK_NEXT` instead of `CHECK-NEXT`
Patch-mainline: no
References: llvm16

Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 test/Concrete/_testingUtils.c | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/test/Concrete/_testingUtils.c b/test/Concrete/_testingUtils.c
index fa395820..d51c6969 100644
--- a/test/Concrete/_testingUtils.c
+++ b/test/Concrete/_testingUtils.c
@@ -69,12 +69,11 @@ int main(int argc, char *argv[])
         printf("print_i1(0)\n");
         print_i1(0);
         // CHECK: i1(0)
-        // CHECK_NEXT: 0
+        // CHECK-NEXT: 0
 
         printf("print_i1(1)\n");
         print_i1(1);
         // CHECK: i1(1)
-        // CHECK_NEXT: 1
-
+        // CHECK-NEXT: 1
 }
 #endif
-- 
2.43.0


++++++ 0014-Use-APIs-of-newer-LLVM-versions-instead-of-unsupport.patch ++++++
From: Martin Nowack <m.now...@imperial.ac.uk>
Date: Mon, 30 Oct 2023 14:52:37 +0000
Subject: Use APIs of newer LLVM versions instead of unsupported ones
Patch-mainline: no
References: llvm16

Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 include/klee/Expr/Expr.h   |  8 +++++++-
 lib/Core/Executor.cpp      | 18 ++++++++++++++++++
 lib/Module/LowerSwitch.cpp | 14 ++++++--------
 lib/Module/RaiseAsm.cpp    |  6 ++++++
 4 files changed, 37 insertions(+), 9 deletions(-)

diff --git a/include/klee/Expr/Expr.h b/include/klee/Expr/Expr.h
index 15075eb8..eb936c3d 100644
--- a/include/klee/Expr/Expr.h
+++ b/include/klee/Expr/Expr.h
@@ -1117,7 +1117,13 @@ public:
   }
 
   /// isAllOnes - Is this constant all ones.
-  bool isAllOnes() const { return getAPValue().isAllOnesValue(); }
+  bool isAllOnes() const {
+#if LLVM_VERSION_CODE <= LLVM_VERSION(13, 0)
+    return getAPValue().isAllOnesValue();
+#else
+    return getAPValue().isAllOnes();
+#endif
+  }
 
   /* Constant Operations */
 
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 58c15141..792b0c76 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2985,7 +2985,11 @@ void Executor::executeInstruction(ExecutionState &state, 
KInstruction *ki) {
     llvm::APFloat Arg(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue());
     uint64_t value = 0;
     bool isExact = true;
+#if LLVM_VERSION_CODE >= LLVM_VERSION(16, 0)
+    auto valueRef = llvm::MutableArrayRef(value);
+#else
     auto valueRef = makeMutableArrayRef(value);
+#endif
     Arg.convertToInteger(valueRef, resultType, false,
                          llvm::APFloat::rmTowardZero, &isExact);
     bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
@@ -3003,7 +3007,11 @@ void Executor::executeInstruction(ExecutionState &state, 
KInstruction *ki) {
 
     uint64_t value = 0;
     bool isExact = true;
+#if LLVM_VERSION_CODE >= LLVM_VERSION(16, 0)
+    auto valueRef = llvm::MutableArrayRef(value);
+#else
     auto valueRef = makeMutableArrayRef(value);
+#endif
     Arg.convertToInteger(valueRef, resultType, true,
                          llvm::APFloat::rmTowardZero, &isExact);
     bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
@@ -4846,7 +4854,12 @@ size_t Executor::getAllocationAlignment(const 
llvm::Value *allocSite) const {
       type = GO->getType();
     }
   } else if (const AllocaInst *AI = dyn_cast<AllocaInst>(allocSite)) {
+#if LLVM_VERSION_CODE <= LLVM_VERSION(10, 0)
     alignment = AI->getAlignment();
+
+#else
+    alignment = AI->getAlign().value();
+#endif
     type = AI->getAllocatedType();
   } else if (isa<InvokeInst>(allocSite) || isa<CallInst>(allocSite)) {
     // FIXME: Model the semantics of the call to use the right alignment
@@ -4869,7 +4882,12 @@ size_t Executor::getAllocationAlignment(const 
llvm::Value *allocSite) const {
     assert(type != NULL);
     // No specified alignment. Get the alignment for the type.
     if (type->isSized()) {
+#if LLVM_VERSION_CODE >= LLVM_VERSION(16, 0)
+      alignment = kmodule->targetData->getPrefTypeAlign(type).value();
+#else
       alignment = kmodule->targetData->getPrefTypeAlignment(type);
+#endif
+
     } else {
       klee_warning_once(allocSite, "Cannot determine memory alignment for "
                                    "\"%s\". Using alignment of %zu.",
diff --git a/lib/Module/LowerSwitch.cpp b/lib/Module/LowerSwitch.cpp
index 84b04b24..f8473156 100644
--- a/lib/Module/LowerSwitch.cpp
+++ b/lib/Module/LowerSwitch.cpp
@@ -70,9 +70,8 @@ void LowerSwitchPass::switchConvert(CaseItr begin, CaseItr 
end,
 
   // iterate through all the cases, creating a new BasicBlock for each
   for (CaseItr it = begin; it < end; ++it) {
-    BasicBlock *newBlock = BasicBlock::Create(F->getContext(), "NodeBlock");
-    Function::iterator FI = origBlock->getIterator();
-    F->getBasicBlockList().insert(++FI, newBlock);
+    BasicBlock *newBlock = BasicBlock::Create(F->getContext(), "NodeBlock", F);
+
     Builder.SetInsertPoint(newBlock);
     auto cmpValue = Builder.CreateICmpEQ(value, it->value, "case.cmp");
     Builder.CreateCondBr(cmpValue, it->block, curHead);
@@ -106,10 +105,10 @@ void LowerSwitchPass::processSwitchInst(SwitchInst *SI) {
 
   // Create a new, empty default block so that the new hierarchy of
   // if-then statements go to this and the PHI nodes are happy.
-  BasicBlock* newDefault = BasicBlock::Create(F->getContext(), "newDefault");
+  BasicBlock *newDefault =
+      BasicBlock::Create(F->getContext(), "newDefault", F, defaultBlock);
   llvm::IRBuilder<> Builder(newDefault);
 
-  F->getBasicBlockList().insert(defaultBlock->getIterator(), newDefault);
   Builder.CreateBr(defaultBlock);
 
   // If there is an entry in any PHI nodes for the default edge, make sure
@@ -132,11 +131,10 @@ void LowerSwitchPass::processSwitchInst(SwitchInst *SI) {
   //   the if comparisons will happen in the same order
   //   as the cases appear in the switch
   std::reverse(cases.begin(), cases.end());
-  
-  switchConvert(cases.begin(), cases.end(), switchValue, origBlock, 
newDefault);
 
+  switchConvert(cases.begin(), cases.end(), switchValue, origBlock, 
newDefault);
   // We are now done with the switch instruction, so delete it
-  origBlock->getInstList().erase(SI);
+  SI->eraseFromParent();
 }
 
 }
diff --git a/lib/Module/RaiseAsm.cpp b/lib/Module/RaiseAsm.cpp
index ec447bc4..799218c9 100644
--- a/lib/Module/RaiseAsm.cpp
+++ b/lib/Module/RaiseAsm.cpp
@@ -91,8 +91,14 @@ bool RaiseAsmPass::runOnModule(Module &M) {
     klee_warning("Warning: unable to select target: %s", Err.c_str());
     TLI = 0;
   } else {
+#if LLVM_VERSION_CODE >= LLVM_VERSION(16, 0)
+    TM = Target->createTargetMachine(TargetTriple, "", "", TargetOptions(),
+                                     std::nullopt);
+#else
     TM = Target->createTargetMachine(TargetTriple, "", "", TargetOptions(),
                                      None);
+#endif
+
     TLI = TM->getSubtargetImpl(*(M.begin()))->getTargetLowering();
 
     triple = llvm::Triple(TargetTriple);
-- 
2.43.0


++++++ 0015-Add-support-for-Intrinsic-get_rounding-for-LLVM-16.patch ++++++
From: Martin Nowack <m.now...@imperial.ac.uk>
Date: Mon, 30 Oct 2023 14:53:48 +0000
Subject: Add support for `Intrinsic::get_rounding` for LLVM 16
Patch-mainline: no
References: llvm16

`Intrinsic::flt_rounds` got removed

Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 lib/Module/IntrinsicCleaner.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp
index 40ff2874..af77ed70 100644
--- a/lib/Module/IntrinsicCleaner.cpp
+++ b/lib/Module/IntrinsicCleaner.cpp
@@ -366,7 +366,11 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, 
Module &M) {
       case Intrinsic::experimental_noalias_scope_decl:
 #endif
       case Intrinsic::floor:
+#if LLVM_VERSION_CODE < LLVM_VERSION(16, 0)
       case Intrinsic::flt_rounds:
+#else
+      case Intrinsic::get_rounding:
+#endif
       case Intrinsic::frameaddress:
       case Intrinsic::get_dynamic_area_offset:
       case Intrinsic::invariant_end:
-- 
2.43.0


++++++ 0016-Add-support-to-aligned_alloc-generated-by-LLVM.patch ++++++
From: Martin Nowack <m.now...@imperial.ac.uk>
Date: Mon, 30 Oct 2023 14:54:46 +0000
Subject: Add support to `aligned_alloc` generated by LLVM
Patch-mainline: no
References: llvm16

Handle like `memalign` for now.

Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 lib/Core/SpecialFunctionHandler.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/lib/Core/SpecialFunctionHandler.cpp 
b/lib/Core/SpecialFunctionHandler.cpp
index 488fba51..79a86112 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -87,6 +87,7 @@ static constexpr std::array handlerInfo = {
   addDNR("klee_abort", handleAbort),
   addDNR("klee_silent_exit", handleSilentExit),
   addDNR("klee_report_error", handleReportError),
+  add("aligned_alloc", handleMemalign, true),
   add("calloc", handleCalloc, true),
   add("free", handleFree, false),
   add("klee_assume", handleAssume, false),
-- 
2.43.0


++++++ 0017-Disable-unsupported-passes-for-newer-LLVM-versions.patch ++++++
From: Martin Nowack <m.now...@imperial.ac.uk>
Date: Mon, 30 Oct 2023 14:56:27 +0000
Subject: Disable unsupported passes for newer LLVM versions
Patch-mainline: no
References: llvm16

Similar functionality needs to be added using a new pass manager

Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 lib/Module/OptimizeLegacy.cpp | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/lib/Module/OptimizeLegacy.cpp b/lib/Module/OptimizeLegacy.cpp
index 53488924..20c8ac2a 100644
--- a/lib/Module/OptimizeLegacy.cpp
+++ b/lib/Module/OptimizeLegacy.cpp
@@ -98,14 +98,18 @@ static void AddStandardCompilePasses(legacy::PassManager 
&PM) {
   addPass(PM, createInstructionCombiningPass()); // Clean up after IPCP & DAE
   addPass(PM, createCFGSimplificationPass());    // Clean up after IPCP & DAE
 
+#if LLVM_VERSION_CODE <= LLVM_VERSION(15, 0)
   addPass(PM, createPruneEHPass()); // Remove dead EH info
+#endif
   addPass(PM, createPostOrderFunctionAttrsLegacyPass());
   addPass(PM,
           createReversePostOrderFunctionAttrsPass()); // Deduce function attrs
 
   if (!DisableInline)
     addPass(PM, createFunctionInliningPass()); // Inline small functions
-  addPass(PM, createArgumentPromotionPass());  // Scalarize uninlined fn args
+#if LLVM_VERSION_CODE <= LLVM_VERSION(14, 0)
+  addPass(PM, createArgumentPromotionPass()); // Scalarize uninlined fn args
+#endif
 
   addPass(PM, createInstructionCombiningPass()); // Cleanup for scalarrepl.
   addPass(PM, createJumpThreadingPass());        // Thread jumps.
@@ -118,7 +122,9 @@ static void AddStandardCompilePasses(legacy::PassManager 
&PM) {
   addPass(PM, createReassociatePass());         // Reassociate expressions
   addPass(PM, createLoopRotatePass());
   addPass(PM, createLICMPass());         // Hoist loop invariants
+#if LLVM_VERSION_CODE <= LLVM_VERSION(14, 0)
   addPass(PM, createLoopUnswitchPass()); // Unswitch loops.
+#endif
   // FIXME : Removing instcombine causes nestedloop regression.
   addPass(PM, createInstructionCombiningPass());
   addPass(PM, createIndVarSimplifyPass());       // Canonicalize indvars
@@ -197,13 +203,17 @@ void klee::optimizeModule(llvm::Module *M,
   if (!DisableInline)
     addPass(Passes, createFunctionInliningPass()); // Inline small functions
 
-  addPass(Passes, createPruneEHPass());         // Remove dead EH info
+#if LLVM_VERSION_CODE <= LLVM_VERSION(15, 0)
+  addPass(Passes, createPruneEHPass()); // Remove dead EH info
+#endif
   addPass(Passes, createGlobalOptimizerPass()); // Optimize globals again.
   addPass(Passes, createGlobalDCEPass());       // Remove dead functions
 
+#if LLVM_VERSION_CODE <= LLVM_VERSION(14, 0)
   // If we didn't decide to inline a function, check to see if we can
   // transform it to pass arguments by value instead of by reference.
   addPass(Passes, createArgumentPromotionPass());
+#endif
 
   // The IPO passes may leave cruft around.  Clean up after them.
   addPass(Passes, createInstructionCombiningPass());
-- 
2.43.0


++++++ 0018-Disable-2018-10-30-llvm-pr39177.ll-for-newer-LLVM-ve.patch ++++++
From: Martin Nowack <m.now...@imperial.ac.uk>
Date: Mon, 30 Oct 2023 14:57:41 +0000
Subject: Disable `2018-10-30-llvm-pr39177.ll` for newer LLVM versions.
Patch-mainline: no
References: llvm16

The optimiser generates different code and calls fwrite directly instead.

Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 test/regression/2018-10-30-llvm-pr39177.ll | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/test/regression/2018-10-30-llvm-pr39177.ll 
b/test/regression/2018-10-30-llvm-pr39177.ll
index 027d0d30..b28947ab 100644
--- a/test/regression/2018-10-30-llvm-pr39177.ll
+++ b/test/regression/2018-10-30-llvm-pr39177.ll
@@ -1,5 +1,7 @@
+; REQUIRES: lt-llvm-15.0
+; The optimizer is more efficient and uses fwrite directly in newer LLVM 
versions
 ; RUN: rm -rf %t.klee-out
-; RUN: %llvmas -f %s -o - | %klee -optimize -output-dir=%t.klee-out | 
FileCheck %s
+; RUN: %klee -optimize -output-dir=%t.klee-out %s | FileCheck %s
 target datalayout = 
"e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64-S128"
 target triple = "x86_64-unknown-linux-gnu"
 
-- 
2.43.0


++++++ 0019-Handle-check-for-thrown-libc-exceptions-more-general.patch ++++++
From: Martin Nowack <m.now...@imperial.ac.uk>
Date: Mon, 30 Oct 2023 14:59:07 +0000
Subject: Handle check for thrown libc++ exceptions more general
Patch-mainline: no
References: llvm16

The wording changed slightly in newer versions.
Update the test case to support this.

Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 test/CXX/symex/libc++/nested_fail.cpp           | 2 +-
 test/CXX/symex/libc++/simple_exception_fail.cpp | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/test/CXX/symex/libc++/nested_fail.cpp 
b/test/CXX/symex/libc++/nested_fail.cpp
index 4dce0279..fe2df4c9 100644
--- a/test/CXX/symex/libc++/nested_fail.cpp
+++ b/test/CXX/symex/libc++/nested_fail.cpp
@@ -24,4 +24,4 @@ int main(int argc, char **args) {
   }
   return 0;
 }
-// CHECK: terminating with uncaught exception of type char*
+// CHECK: terminating {{.*}} uncaught exception of type char*
diff --git a/test/CXX/symex/libc++/simple_exception_fail.cpp 
b/test/CXX/symex/libc++/simple_exception_fail.cpp
index 793d9201..c3e295c2 100644
--- a/test/CXX/symex/libc++/simple_exception_fail.cpp
+++ b/test/CXX/symex/libc++/simple_exception_fail.cpp
@@ -11,4 +11,4 @@
 int main(int argc, char **args) {
   throw std::runtime_error("foo");
 }
-// CHECK: terminating with uncaught exception of type std::runtime_error: foo
\ No newline at end of file
+// CHECK: terminating {{.*}} uncaught exception of type std::runtime_error: foo
\ No newline at end of file
-- 
2.43.0


++++++ 0020-Update-test-case-for-expressions-using-udiv-urem-sdi.patch ++++++
From: Martin Nowack <m.now...@imperial.ac.uk>
Date: Mon, 30 Oct 2023 15:00:58 +0000
Subject: Update test case for expressions using `udiv`, `urem`, `sdiv` and
 `srem`
Patch-mainline: no
References: llvm16

They are not supported anymore for newer LLVM versions.

Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 test/Concrete/ConstantExpr.ll    |  29 +-----
 test/Concrete/ConstantExprOld.ll | 166 +++++++++++++++++++++++++++++++
 2 files changed, 167 insertions(+), 28 deletions(-)
 create mode 100644 test/Concrete/ConstantExprOld.ll

diff --git a/test/Concrete/ConstantExpr.ll b/test/Concrete/ConstantExpr.ll
index efe9f141..b85ce36a 100644
--- a/test/Concrete/ConstantExpr.ll
+++ b/test/Concrete/ConstantExpr.ll
@@ -1,3 +1,4 @@
+; REQUIRES: geq-llvm-15.0
 ; RUN: %S/ConcreteTest.py --klee='%klee' --lli=%lli %s
 
 ; Most of the test below use the *address* of gInt as part of their 
computation,
@@ -86,32 +87,6 @@ define void @"test_simple_arith"() {
 
   ret void     
 }
-
-define void @"test_div_and_mod"() {
-  %t1 = add i32 udiv(i32 ptrtoint(i32* @gInt to i32), i32 13), 0
-  %t2 = add i32 urem(i32 ptrtoint(i32* @gInt to i32), i32 13), 0
-  %t3 = add i32 sdiv(i32 ptrtoint(i32* @gInt to i32), i32 13), 0
-  %t4 = add i32 srem(i32 ptrtoint(i32* @gInt to i32), i32 13), 0
-
-  %p = ptrtoint i32* @gInt to i32
-
-  %i1 = udiv i32 %p, 13
-  %i2 = urem i32 %p, 13
-  %i3 = sdiv i32 %p, 13
-  %i4 = srem i32 %p, 13
-
-  %x1 = sub i32 %t1, %i1
-  %x2 = sub i32 %t2, %i2
-  %x3 = sub i32 %t3, %i3
-  %x4 = sub i32 %t4, %i4
-
-  call void @print_i32(i32 %x1)
-  call void @print_i32(i32 %x2)
-  call void @print_i32(i32 %x3)
-  call void @print_i32(i32 %x4)
-
-  ret void     
-}
         
 define void @test_cmp() {
   %t1 = add i8 zext(i1 icmp ult (i64 ptrtoint(i32* @gInt to i64), i64 0) to 
i8), 1
@@ -142,8 +117,6 @@ define void @test_cmp() {
 define i32 @main() {
     call void @test_simple_arith()
 
-    call void @test_div_and_mod()
-
     call void @test_cmp()
  
     call void @test_int_to_ptr()
diff --git a/test/Concrete/ConstantExprOld.ll b/test/Concrete/ConstantExprOld.ll
new file mode 100644
index 00000000..2e6438bc
--- /dev/null
+++ b/test/Concrete/ConstantExprOld.ll
@@ -0,0 +1,166 @@
+; REQUIRES: lt-llvm-15.0
+; RUN: %S/ConcreteTest.py --klee='%klee' --lli=%lli %s
+
+; Most of the test below use the *address* of gInt as part of their 
computation,
+; and then perform some operation (like x | ~x) which makes the result
+; deterministic. They do, however, assume that the sign bit of the address as a
+; 64-bit value will never be set.
+@gInt = global i32 10
+@gIntWithConstant = global i32 sub(i32 ptrtoint(i32* @gInt to i32), 
+                                 i32 ptrtoint(i32* @gInt to i32))
+
+define void @"test_int_to_ptr"() {
+  %t1 = add i8 ptrtoint(i8* inttoptr(i32 100 to i8*) to i8), 0
+  %t2 = add i32 ptrtoint(i32* inttoptr(i8 100 to i32*) to i32), 0
+  %t3 = add i32 ptrtoint(i32* inttoptr(i64 100 to i32*) to i32), 0
+  %t4 = add i64 ptrtoint(i8* inttoptr(i32 100 to i8*) to i64), 0
+
+  call void @print_i8(i8 %t1)
+  call void @print_i32(i32 %t2)
+  call void @print_i32(i32 %t3)
+  call void @print_i64(i64 %t4)
+    
+  ret void
+}
+
+define void @"test_constant_ops"() {
+  %t1 = add i8 trunc(i64 add(i64 ptrtoint(i32* @gInt to i64), i64 -10) to i8), 
10
+  %t2 = and i64 sub(i64 sext(i32 ptrtoint(i32* @gInt to i32) to i64), i64 
ptrtoint(i32* @gInt to i64)), 4294967295
+  %t3 = and i64 sub(i64 zext(i32 ptrtoint(i32* @gInt to i32) to i64), i64 
ptrtoint(i32* @gInt to i64)), 4294967295
+
+  %t4 = icmp eq i8 trunc(i64 ptrtoint(i32* @gInt to i64) to i8), %t1
+  %t5 = zext i1 %t4 to i8
+    
+  call void @print_i8(i8 %t5)
+  call void @print_i64(i64 %t2)
+  call void @print_i64(i64 %t3)
+  
+  ret void
+}
+
+define void @"test_logical_ops"() {
+  %t1 = add i32 -10, and(i32 ptrtoint(i32* @gInt to i32), i32 xor(i32 
ptrtoint(i32* @gInt to i32), i32 -1))
+  %t2 = add i32 -10, or(i32 ptrtoint(i32* @gInt to i32), i32 xor(i32 
ptrtoint(i32* @gInt to i32), i32 -1))
+  %t3 = add i32 -10, xor(i32 xor(i32 ptrtoint(i32* @gInt to i32), i32 1024),  
i32 ptrtoint(i32* @gInt to i32))
+
+  call void @print_i32(i32 %t1)
+  call void @print_i32(i32 %t2)
+  call void @print_i32(i32 %t3)
+
+  ; or the address with 1 to ensure the addresses will differ in 'ne' below
+  %t4 = shl i64 lshr(i64 or(i64 ptrtoint(i32* @gInt to i64), i64 1), i64 8), 8
+  %t5 = shl i64 ashr(i64 or(i64 ptrtoint(i32* @gInt to i64), i64 1), i64 8), 8
+  %t6 = lshr i64 shl(i64 or(i64 ptrtoint(i32* @gInt to i64), i64 1), i64 8), 8
+  
+  %t7 = icmp eq i64 %t4, %t5
+  %t8 = icmp ne i64 %t4, %t6
+  
+  %t9 = zext i1 %t7 to i8
+  %t10 = zext i1 %t8 to i8
+  
+  call void @print_i8(i8 %t9)
+  call void @print_i8(i8 %t10)
+  
+  ret void   
+}
+
+%test.struct.type = type { i32, i32 }
+@test_struct = global %test.struct.type { i32 0, i32 10 }
+
+define void @"test_misc"() {
+  ; probability that @gInt == 100 is very very low 
+  %t1 = add i32 select(i1 icmp eq (i32* @gInt, i32* inttoptr(i32 100 to 
i32*)), i32 10, i32 0), 0
+  call void @print_i32(i32 %t1)
+
+  %t2 = load i32, i32* getelementptr(%test.struct.type, %test.struct.type* 
@test_struct, i32 0, i32 1)
+  call void @print_i32(i32 %t2)                             
+        
+  ret void
+}
+
+define void @"test_simple_arith"() {
+  %t1 = add i32 add(i32 ptrtoint(i32* @gInt to i32), i32 0), 0
+  %t2 = add i32 sub(i32 0, i32 ptrtoint(i32* @gInt to i32)), %t1
+  %t3 = mul i32 mul(i32 ptrtoint(i32* @gInt to i32), i32 10), %t2
+
+  call void @print_i32(i32 %t3)
+
+  ret void     
+}
+
+define void @"test_div_and_mod"() {
+  %t1 = add i32 udiv(i32 ptrtoint(i32* @gInt to i32), i32 13), 0
+  %t2 = add i32 urem(i32 ptrtoint(i32* @gInt to i32), i32 13), 0
+  %t3 = add i32 sdiv(i32 ptrtoint(i32* @gInt to i32), i32 13), 0
+  %t4 = add i32 srem(i32 ptrtoint(i32* @gInt to i32), i32 13), 0
+
+  %p = ptrtoint i32* @gInt to i32
+
+  %i1 = udiv i32 %p, 13
+  %i2 = urem i32 %p, 13
+  %i3 = sdiv i32 %p, 13
+  %i4 = srem i32 %p, 13
+
+  %x1 = sub i32 %t1, %i1
+  %x2 = sub i32 %t2, %i2
+  %x3 = sub i32 %t3, %i3
+  %x4 = sub i32 %t4, %i4
+
+  call void @print_i32(i32 %x1)
+  call void @print_i32(i32 %x2)
+  call void @print_i32(i32 %x3)
+  call void @print_i32(i32 %x4)
+
+  ret void     
+}
+        
+define void @test_cmp() {
+  %t1 = add i8 zext(i1 icmp ult (i64 ptrtoint(i32* @gInt to i64), i64 0) to 
i8), 1
+  %t2 = add i8 zext(i1 icmp ule (i64 ptrtoint(i32* @gInt to i64), i64 0) to 
i8), 1
+  %t3 = add i8 zext(i1 icmp uge (i64 ptrtoint(i32* @gInt to i64), i64 0) to 
i8), 1
+  %t4 = add i8 zext(i1 icmp ugt (i64 ptrtoint(i32* @gInt to i64), i64 0) to 
i8), 1
+  %t5 = add i8 zext(i1 icmp slt (i64 ptrtoint(i32* @gInt to i64), i64 0) to 
i8), 1
+  %t6 = add i8 zext(i1 icmp sle (i64 ptrtoint(i32* @gInt to i64), i64 0) to 
i8), 1
+  %t7 = add i8 zext(i1 icmp sge (i64 ptrtoint(i32* @gInt to i64), i64 0) to 
i8), 1
+  %t8 = add i8 zext(i1 icmp sgt (i64 ptrtoint(i32* @gInt to i64), i64 0) to 
i8), 1
+  %t9 = add i8 zext(i1 icmp eq (i64 ptrtoint(i32* @gInt to i64), i64 10) to 
i8), 1
+  %t10 = add i8 zext(i1 icmp ne (i64 ptrtoint(i32* @gInt to i64), i64 10) to 
i8), 1
+
+  call void @print_i1(i8 %t1)
+  call void @print_i1(i8 %t2)
+  call void @print_i1(i8 %t3)
+  call void @print_i1(i8 %t4)
+  call void @print_i1(i8 %t5)
+  call void @print_i1(i8 %t6)
+  call void @print_i1(i8 %t7)
+  call void @print_i1(i8 %t8)
+  call void @print_i1(i8 %t9)
+  call void @print_i1(i8 %t10)
+
+  ret void
+}
+
+define i32 @main() {
+    call void @test_simple_arith()
+
+    call void @test_div_and_mod()
+
+    call void @test_cmp()
+ 
+    call void @test_int_to_ptr()
+
+    call void @test_constant_ops()
+
+    call void @test_logical_ops()
+
+    call void @test_misc()
+    
+    ret i32 0
+}
+
+; defined in print_int.c
+declare void @print_i1(i8)
+declare void @print_i8(i8)
+declare void @print_i16(i16)
+declare void @print_i32(i32)
+declare void @print_i64(i64)
-- 
2.43.0


++++++ 0021-Support-newer-LLVM-versions-in-lit.patch ++++++
From: Martin Nowack <m.now...@imperial.ac.uk>
Date: Mon, 30 Oct 2023 15:02:08 +0000
Subject: Support newer LLVM versions in `lit`
Patch-mainline: no
References: llvm16

Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 test/lit.cfg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/lit.cfg b/test/lit.cfg
index c442c409..ec654a47 100644
--- a/test/lit.cfg
+++ b/test/lit.cfg
@@ -164,7 +164,7 @@ config.substitutions.append(
 
 # Add feature for the LLVM version in use, so it can be tested in REQUIRES and
 # XFAIL checks. We also add "not-XXX" variants, for the same reason.
-known_llvm_versions = { "9.0", "10.0", "11.0", "11.1", "12.0", "13.0", "14.0" }
+known_llvm_versions = { "9.0", "10.0", "11.0", "11.1", "12.0", "13.0", "14.0", 
"15.0", "16.0", "17.0" }
 current_llvm_version_tuple = (int(config.llvm_version_major), 
int(config.llvm_version_minor))
 current_llvm_version = "%s.%s" % current_llvm_version_tuple
 
-- 
2.43.0


++++++ 0022-Enable-CI-to-test-newer-LLVM-versions.patch ++++++
From: Martin Nowack <m.now...@imperial.ac.uk>
Date: Mon, 30 Oct 2023 15:03:34 +0000
Subject: Enable CI to test newer LLVM versions
Patch-mainline: no
References: llvm16

Signed-off-by: Jiri Slaby <jsl...@suse.cz>
---
 .github/workflows/build.yaml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml
index fa924a37..a329a02c 100644
--- a/.github/workflows/build.yaml
+++ b/.github/workflows/build.yaml
@@ -36,6 +36,8 @@ jobs:
     strategy:
       matrix:
         name: [
+          "LLVM 16",
+          "LLVM 15",
           "LLVM 14",
           "LLVM 13",
           "LLVM 12",
@@ -53,6 +55,12 @@ jobs:
           "No TCMalloc, optimised runtime",
         ]
         include:
+          - name: "LLVM 16"
+            env:
+              LLVM_VERSION: 16
+          - name: "LLVM 15"
+            env:
+              LLVM_VERSION: 15
           - name: "LLVM 14"
             env:
               LLVM_VERSION: 14
-- 
2.43.0


++++++ FileCheck.cpp ++++++
--- /var/tmp/diff_new_pack.xFDEff/_old  2023-12-21 23:39:19.824108094 +0100
+++ /var/tmp/diff_new_pack.xFDEff/_new  2023-12-21 23:39:19.828108240 +0100
@@ -18,7 +18,9 @@
 #include "llvm/FileCheck/FileCheck.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/InitLLVM.h"
+#include "llvm/Support/MemoryBuffer.h"
 #include "llvm/Support/Process.h"
+#include "llvm/Support/SourceMgr.h"
 #include "llvm/Support/WithColor.h"
 #include "llvm/Support/raw_ostream.h"
 #include <cmath>
@@ -79,7 +81,7 @@
              "checks that some error message does not occur, for example."));
 
 static cl::opt<bool> AllowUnusedPrefixes(
-    "allow-unused-prefixes", cl::init(false), cl::ZeroOrMore,
+    "allow-unused-prefixes",
     cl::desc("Allow prefixes to be specified but not appear in the test."));
 
 static cl::opt<bool> MatchFullLines(
@@ -102,12 +104,12 @@
              "non-overlapping CHECK-DAG implementation.\n"));
 
 static cl::opt<bool> Verbose(
-    "v", cl::init(false), cl::ZeroOrMore,
+    "v",
     cl::desc("Print directive pattern matches, or add them to the input dump\n"
              "if enabled.\n"));
 
 static cl::opt<bool> VerboseVerbose(
-    "vv", cl::init(false), cl::ZeroOrMore,
+    "vv",
     cl::desc("Print information helpful in diagnosing internal FileCheck\n"
              "issues, or add it to the input dump if enabled.  Implies\n"
              "-v.\n"));
@@ -367,6 +369,8 @@
     return "bad-not";
   case Check::CheckBadCount:
     return "bad-count";
+  case Check::CheckMisspelled:
+    return "misspelled";
   case Check::CheckNone:
     llvm_unreachable("invalid FileCheckType");
   }
@@ -630,7 +634,7 @@
     // -dump-input-filter.  However, in case the resulting ellipsis would 
occupy
     // more lines than the input lines and annotations it elides, buffer the
     // elided lines and annotations so we can print them instead.
-    raw_ostream *LineOS = &OS;
+    raw_ostream *LineOS;
     if ((!PrevLineInFilter || PrevLineInFilter + DumpInputContext < Line) &&
         (NextLineInFilter == UINT_MAX ||
          Line + DumpInputContext < NextLineInFilter))

++++++ _service ++++++
--- /var/tmp/diff_new_pack.xFDEff/_old  2023-12-21 23:39:19.848108971 +0100
+++ /var/tmp/diff_new_pack.xFDEff/_new  2023-12-21 23:39:19.852109117 +0100
@@ -1,5 +1,5 @@
 <services>
-  <service name="obs_scm" mode="disabled">
+  <service name="obs_scm" mode="manual">
     <param name="url">https://github.com/klee/klee</param>
     <param name="scm">git</param>
     <param name="changesgenerate">enable</param>
@@ -7,7 +7,7 @@
     <param name="versionrewrite-pattern">v(.*)</param>
     <param name="versionrewrite-replacement">\1</param>
   </service>
-  <service name="set_version" mode="disabled" />
+  <service name="set_version" mode="manual" />
 
   <service name="tar" mode="buildtime"/>
   <service name="recompress" mode="buildtime">

++++++ _servicedata ++++++
--- /var/tmp/diff_new_pack.xFDEff/_old  2023-12-21 23:39:19.868109701 +0100
+++ /var/tmp/diff_new_pack.xFDEff/_new  2023-12-21 23:39:19.872109847 +0100
@@ -1,6 +1,6 @@
 <servicedata>
 <service name="tar_scm">
                 <param name="url">https://github.com/klee/klee</param>
-              <param 
name="changesrevision">c10e9e926700773e01f44fbb1917deac7be2aaea</param></service></servicedata>
+              <param 
name="changesrevision">fc83f06b17221bf5ef20e30d9da1ccff927beb17</param></service></servicedata>
 (No newline at EOF)
 

++++++ klee-3.0+20230611.obscpio -> klee-3.0+20231023.obscpio ++++++
/work/SRC/openSUSE:Factory/klee/klee-3.0+20230611.obscpio 
/work/SRC/openSUSE:Factory/.klee.new.1840/klee-3.0+20231023.obscpio differ: 
char 48, line 1

++++++ klee-rpmlintrc ++++++
--- /var/tmp/diff_new_pack.xFDEff/_old  2023-12-21 23:39:19.908111162 +0100
+++ /var/tmp/diff_new_pack.xFDEff/_new  2023-12-21 23:39:19.912111308 +0100
@@ -1,3 +1,2 @@
-addFilter("shlib-policy-name-error .*libkleeRuntest")
 addFilter("devel-file-in-non-devel-package")
 

++++++ klee.obsinfo ++++++
--- /var/tmp/diff_new_pack.xFDEff/_old  2023-12-21 23:39:19.928111892 +0100
+++ /var/tmp/diff_new_pack.xFDEff/_new  2023-12-21 23:39:19.932112038 +0100
@@ -1,5 +1,5 @@
 name: klee
-version: 3.0+20230611
-mtime: 1686507804
-commit: c10e9e926700773e01f44fbb1917deac7be2aaea
+version: 3.0+20231023
+mtime: 1698093351
+commit: fc83f06b17221bf5ef20e30d9da1ccff927beb17
 

++++++ not.cpp ++++++
--- /var/tmp/diff_new_pack.xFDEff/_old  2023-12-21 23:39:19.948112622 +0100
+++ /var/tmp/diff_new_pack.xFDEff/_new  2023-12-21 23:39:19.952112768 +0100
@@ -58,7 +58,8 @@
   for (int i = 0; i < argc; ++i)
     Argv.push_back(argv[i]);
   std::string ErrMsg;
-  int Result = sys::ExecuteAndWait(*Program, Argv, None, {}, 0, 0, &ErrMsg);
+  int Result =
+      sys::ExecuteAndWait(*Program, Argv, std::nullopt, {}, 0, 0, &ErrMsg);
 #ifdef _WIN32
   // Handle abort() in msvcrt -- It has exit code as 3.  abort(), aka
   // unreachable, should be recognized as a crash.  However, some binaries use

Reply via email to