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@localhost:~/tests/klee_dev> clang --version clang version 17.0.1 Target: x86_64-suse-linux Thread model: posix InstalledDir: /usr/bin linux@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@localhost:~/tests/klee_dev> linux@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@localhost:~/tests/klee_dev> clang -I ../../include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone get_sign.c linux@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@localhost:~/tests/klee_dev> or linux@localhost:~/tests/klee_dev> clang -emit-llvm -c get_sign.c linux@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@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@localhost:~/tests/klee_dev> sudo zypper install clang14 that works linux@localhost:~/tests/klee_dev> clang-14 -I ../../include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone get_sign.c linux@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@localhost:~/tests/klee_dev> any idea how to solve the opaque pointer error without using the older clang-14? _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
