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

[Nowack, Martin]

Hi Dennis,

KLEE currently doesn’t support newer LLVM versions than 14.
We are working on this but it’s not in a stage for upstreaming it yet.

Unfortunately you have to stick with LLVM 14 in this case.

Best,
Martin


> On 1. Oct 2023, at 11:23, Dennis Luehring <dl.soluz at gmx.net> wrote:
> 
> 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?
> 
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev