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

Reply via email to