[klee-dev] can't get the get_sign.c to work under Tumbleweed Suse with clang-17

[Dennis Luehring]

Standard Clang 17.0.1 and Klee 3.0 from Tumbleweed package manager
per default the klee packages comes with LLVM 14.0.6


linux at localhost:~/tests/klee_dev> clang --version
clang version 17.0.1
Target: x86_64-suse-linux
Thread model: posix
InstalledDir: /usr/bin

linux at localhost:~/tests/klee_dev> klee --version
KLEE 3.1-pre (https://klee.github.io)
   Build mode: RelWithDebInfo (Asserts: OFF)
   Build revision: unknown

LLVM (http://llvm.org/):
   LLVM version 14.0.6
   Optimized build.
   Default target: x86_64-suse-linux
   Host CPU: rocketlake
linux at localhost:~/tests/klee_dev>

linux at localhost:~/tests/klee_dev> llvm-cov --version
LLVM (http://llvm.org/):
   LLVM version 17.0.1
   Optimized build.


https://klee.github.io/tutorials/testing-function/
https://github.com/klee/klee/blob/master/examples/get_sign/get_sign.c

following the tutorial

linux at localhost:~/tests/klee_dev> clang -I ../../include -emit-llvm -c
-g -O0 -Xclang -disable-O0-optnone get_sign.c
linux at localhost:~/tests/klee_dev> klee get_sign.bc
KLEE: ERROR: Loading file get_sign.bc failed: Opaque pointers are only
supported in -opaque-pointers mode (Producer: 'LLVM17.0.1' Reader: 'LLVM
14.0.6')
linux at localhost:~/tests/klee_dev>

or

linux at localhost:~/tests/klee_dev> clang -emit-llvm -c get_sign.c
linux at localhost:~/tests/klee_dev> klee get_sign.bc
KLEE: ERROR: Loading file get_sign.bc failed: Opaque pointers are only
supported in -opaque-pointers mode (Producer: 'LLVM17.0.1' Reader: 'LLVM
14.0.6')
linux at localhost:~/tests/klee_dev>

i am not able to disable the opaque pointers according to this doc:
https://llvm.org/docs/OpaquePointers.html

the i installed the older clang-14

linux at localhost:~/tests/klee_dev> sudo zypper install clang14

that works

linux at localhost:~/tests/klee_dev> clang-14 -I ../../include -emit-llvm
-c -g -O0 -Xclang -disable-O0-optnone get_sign.c
linux at localhost:~/tests/klee_dev> klee get_sign.bc
KLEE: output directory is "/home/linux/tests/klee_dev/klee-out-1"
KLEE: Using STP solver backend
KLEE: SAT solver: MiniSat

KLEE: done: total instructions = 33
KLEE: done: completed paths = 3
KLEE: done: partially completed paths = 0
KLEE: done: generated tests = 3
linux at localhost:~/tests/klee_dev>

any idea how to solve the opaque pointer error without using the older
clang-14?