Hi Cristian, On Sat, Feb 7, 2009 at 5:38 PM, Cristian Zamfir <cristian.zamfir at epfl.ch> wrote: > > Hi, > > I have two linking problems. > > The first one is when compiling a program that uses sockets. In my > case, it should be OK if the socket calls/syscalls are executed as > external functions, however, I get this error message: > > KLEE: WARNING: undefined reference to function: __socketcall
The rough answer to this question is that when klee goes to execute an external function call, it eventually drops to LLVM to look that symbol up in the running executable. Essentially, klee cannot call __socketcall because there is no symbol for it in the klee binary (makes sense, since klee doesn't link against the socket library). I believe you can use 'klee ... --load=/path/to/socket/libary.so ...''' to have LLVM automatically use this library as well for symbol resolution. Or you can also modify the Makefiles to link with the socket library. This is all assuming that the socket library defines __socketcall in a manner that matches uclibc, but since for the most part uclibc seems to be a slimmed version of glibc this is probably a safe assumption. > Is there any way to see why the external call failed? A failure means that the function call couldn't be resolved. I believe that for other errors (crash during an external call) a different message is reported; although I might have forgotten. > The second problem is when I compile a library called NL using klee- > gcc and separately a program (also with klee-gcc) that links against > this library. > > I do something like make CC=klee-gcc AR="llvm-ar cru" RANLIB="llvm- > ranlib" to make the library and everything goes ok, no errors. > > Then I simply do "make CC=klee-gcc" for the program that links against > the NL library which in the end runs > llvm-ld --disable-opt -lNL -L../src program.o -o program > Again no errors. The issue here is that llvm-ld is not respecing the -l, I think. Does it work if you use -- llvm-ld --disable-opt ../src/libNL.a program.o -o program -- ? There is no llvm-ldd; however klee never respects the "linked library" list that llvm can embed in files (and asserts if it is non-empty), so the this isn't really the problem. llvm-ld doesn't really function like a regular linker would as far as giving you errors about undefined symbols when you are making an executable, it really just does the symbol merging part of linking. You can use 'llvm-nm' to look at the final image to find out what symbols are still undefined (and the klee warnings at startup). Does this help? - Daniel
