Hi, I am trying to work out if it is possible to use shared libraries with Klee. Specifically, lets say I have an application that calls various library functions - can I mark the input to those external libraries as symbolic and execute both the library and application symbolically?
I have attempted this and got have no success, possibly because Klee doesnt take linked objects in? If I take the simple slightly modified Tutorial 1, and put the function in a shared library I get: Compile library first: llvm-gcc -fPIC -o libltest.so ltest.c -shared and now the test application llvm-gcc --emit-llvm -g main.c -lltest -L. /tmp/ccdlAKaP.o: file not recognized: File format not recognized Klee the object file: klee main.o KLEE: ERROR: /home/jack/libtest/ltest/tester/main.c:9: external call with symbolic argument: test KLEE: NOTE: now ignoring this error at this location This seems fairly expected because the library is not in llvm bitcode, but from what I've read I can't do any linking for the Klee input so I'm pretty confused. Either Klee doesn't support symbolic execution of shared libaries with an application as the start point or im doing something stupid - hopefully it's the latter. I have tried this on larger real world applications and the compile process goes perfectly but as soon as linking starts I get very stuck with libtool reporting unsupportd file formats etc :( Thanks for any help.
_______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
