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

[Dennis Luehring]

Am 02.10.2023 um 16:31 schrieb Nowack, Martin:
> Unfortunately you have to stick with LLVM 14 in this case.

fine - thank you for all the work on Klee

im currently starting to use it to check if i translated 16bit dos
disassembly
correctly to equal C code - Klee helps creating the test-cases

i first stupidly translated the real asm to assembler-semantic and
looking like functions in C
then let Klee find all ways through the code and then test it agains my
C port of it

hope this will be useable for bigger functions in the future

>
> 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
>