> I got the next error messag: > > KLEE: ERROR: unable to load symbol(PC) while initializing globals. > > Could you tell me what should I do then? Thank you very much.
The error message you are seeing comes from lib/Core/Executor.cpp:568 I'm not entirely familiar with how this works but I think what is happening is the following - the "PC" symbol appears to be undefined (because i->isDeclaration() is true) in bash.bc - Because PC is undefined KLEE tries to see if the symbol is present in the running copy of KLEE itself. For example if bash.bc has a undefined symbol __dso_handle then the address it will get is the __dso_handle of the KLEE executable. - There is probably no "PC" symbol in KLEE so it fails. To fix this you need to figure out where the PC symbol is coming from in the bash source code and see if you can remove it from bash.bc or support is some how within KLEE. You should realise that the bash.bc file will have some things missing from it. - Any external static libraries cannot be linked with it (because they will be in a binary format and not LLVM bitcode) - Any external dynamic libraries won't be linked in either. Looking on my system, bash linux, it dynamically links with linux-vdso.so.1 (0x00007fffb810b000) libreadline.so.6 => /usr/lib/libreadline.so.6 (0x00007f5f98041000) libncursesw.so.5 => /usr/lib/libncursesw.so.5 (0x00007f5f97ddc000) libdl.so.2 => /usr/lib/libdl.so.2 (0x00007f5f97bd8000) libc.so.6 => /usr/lib/libc.so.6 (0x00007f5f97830000) /lib64/ld-linux-x86-64.so.2 (0x00007f5f9828b000) so it is likely that your missing symbol is provided by one of these libraries. If you can figure out which library provides that symbol you might be able to hack KLEE by forcing it to dynamically load the right shared libraries (i.e. [1] or dlopen() ) before KLEE tries to initialise the globals of the LLVM bitcode program it is interpreting. [1] http://llvm.org/docs/doxygen/html/classllvm_1_1sys_1_1DynamicLibrary.html Hope that helps, Dan. _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
