Hi, One issue could be that during compilation the wrong include files are used. Make sure you use the include files provided with libc++ implementation you use for KLEE.
Please refer to the following documentation to get further information: https://libcxx.llvm.org/UsingLibcxx.html#using-a-custom-built-libc Best, Martin On 21. Jun 2022, at 15:05, 房合钧 <1106929...@qq.com<mailto:1106929...@qq.com>> wrote: ##### **An error "Unable to load symbol(_ZTVNSt3_18ios_baseE)while initializing globals" occurred when running in klee.** **1.After I use the wllvm tool to compile the packJPG project into an executable file——packJPG, I use its script to convert the packJPG executable file into a bitcode file——packJPG.bc** ``` To ensure that the functionality of the executables obtained by wllvm is not compromised, and consistent with the executables obtained using the project's own build method, I ran them with the same test case and got the same compression ratio. wllvm compile command: $ export LLVM_COMPILER=clang $ export WLLVM_OUPUT=DEBUG $ export CC=/usr/local/bin/wllvm $ export CXX=/usr/local/bin/wllvm++ $ export CFLAGS="-g -O1 -Xclang -disable-llvm-passes -D__NO_STRING_INLINES -D_FORTIFY_SOURCE=0 -U__OPTIMIZE__" $ wllvm++ -c -o bitops.o bitops.cpp -stdlib=libc++ $ wllvm++ -c -o aricoder.o aricoder.cpp -stdlib=libc++ $ wllvm++ -c -o packjpg.o packjpg.cpp -stdlib=libc++ $ wllvm++ -o packJPG bitops.o aricoder.o packjpg.o -stdlib=libc++ -lc++experimental $ export LLVM_LINK_NAME=llvm-link-11 $ export LLVM_AR_NAME=llvm-ar-11 $ extract-bc packJPG ``` **2、When running this bitcode file with klee, the following error occurred:** ``` KLEE:ERROR:Unable to load symbol(_ZTVNSt3_18ios_baseE)while initializing globals ``` I found this symbol in the symbol table of the libc++.so library that the packJPG project depends on. **3、I have tried several methods to solve this error.** ``` (1)Add a parameter of klee to the running command: -link-llvm-lib.But it didn't solve my problem, because turning the system library into a bitcode file is still an expensive method. (2)It is found that the compiler set in the original Makefile of the packJPG project is gcc and the dependent libraries are set to be statically linked. Now I don't know how to migrate the static dependency library (-static-libgcc -static-libstdc++) of the gcc compiler to the static library of the corresponding clang compiler. I tried -static-libc++ but it doesn't seem to work ``` Has anyone encountered this error? Or is there any possible workaround? Expecting a reply! _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk<mailto:klee-dev@imperial.ac.uk> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev