Hi,
On Mon, 8 Aug 2022 18:24:27 -0700 Biqian Cheng <bchen...@ucr.edu> wrote: > Did you rebuild it (make) in case it was wrong beforehand? > > Yes, I tried to use "cmake -DENABLE_POSIX_RUNTIME=ON > -DENABLE_KLEE_UCLIBC=ON -DKLEE_UCLIBC_PATH=/home/klee-uclibc .." then > "make -j2" to rebuild it. I meant uclibc. There is a "make -j2" line in step 5: https://klee.github.io/build-llvm11/ Here you are configuring KLEE. Do a "make clean" in KLEE's build directory and call cmake with your options again but add the path to your llvm-config-11: -DLLVM_CONFIG_BINARY=<path>/bin/llvm-config-11 > Then check the LLVM version klee is linked against (e.g. ldd >> <path>/bin/klee) > > > I used "ldd /usr/local/bin/klee", it gives me: > > ... > libLLVM-10.so.1 => /usr/lib/llvm-10/lib/libLLVM-10.so.1 > (0x00007f183c049000) libstdc++.so.6 => > ... > Is this indicating I'm using LLVM-10, while I'm supposed to use > LLVM-11? Yes. > and finally the build output of your program.bc (enable verbose mode > for > > make/...). > > > Does this mean make -j2? Depending on the Makefile for that program you can run "make VERBOSE=1" or use a hack like "make SHELL='sh -x'" to see what commands are executed. If it's just a single C file and you are using clang directly, you don't need that step. Kind regards, Frank _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
