Hello, Under the help from your team, I think I have built KLEE with LLVM-3.4 successfully, because I could run the first and second tutorial.
However, I also have two problems as following. 1, for the second tutorial(regexp), after I run regexp.bc with the order "KLEE regexp.bc", the result is the following: total instructions = 4598603 completed paths =7438 generated tests = 6677 There exists a big difference with your running result showed on the webpage, total instructions = 6334861 completed paths =7692 generated tests = 22 *Why the number of generated tests is much less than my result? Is it because the computer configuration or my KLEE still exists some errors or other reasons?* 2, When I built Coreutils6.11 with KLEE, I faced the following errors: *make all-am* *make[3]: Entering directory '/home/loveling10/klee/examples/coreutils/coreutils/obj-llvm/lib'* *depbase=`echo areadlink-with-size.o | sed 's|[^/]*$|.deps/&|;s|\.o$||'`;\* */home/loveling10/klee/scripts/klee-gcc -I. -I../../lib -g -MT areadlink-with-size.o -MD -MP -MF $depbase.Tpo -c -o areadlink-with-size.o ../../lib/areadlink-with-size.c &&\* *mv -f $depbase.Tpo $depbase.Po* *Traceback (most recent call last):* * File "/home/loveling10/klee/scripts/klee-gcc", line 34, in <module>* * main()* * File "/home/loveling10/klee/scripts/klee-gcc", line 13, in main* * os.execvp("llvm-gcc", ["llvm-gcc", "-emit-llvm"] + sys.argv[1:])* * File "/usr/lib/python2.7/os.py", line 346, in execvp* * _execvpe(file, args)I* * File "/usr/lib/python2.7/os.py", line 382, in _execvpe* * func(fullname, *argrest)* *OSError: [Errno 2] No such file or directory* *Makefile:1249: recipe for target 'areadlink-with-size.o' failed* *make[3]: *** [areadlink-with-size.o] Error 1* *make[3]: Leaving directory '/home/loveling10/klee/examples/coreutils/coreutils/obj-llvm/lib'* *Makefile:908: recipe for target 'all' failed* *make[2]: *** [all] Error 2* *make[2]: Leaving directory '/home/loveling10/klee/examples/coreutils/coreutils/obj-llvm/lib'* *Makefile:814: recipe for target 'all-recursive' failed* *make[1]: *** [all-recursive] Error 1* *make[1]: Leaving directory '/home/loveling10/klee/examples/coreutils/coreutils/obj-llvm'* *Makefile:769: recipe for target 'all' failed* *make: *** [all] Error 2* I have found one solution from the mail-list. It is said that *LLVM-LD can't find the libraries it needs to link with. In the is case librt * *(the realtime library). Find the location of librt.a on your system and set the LLVM_LIB_SEARCH_PATH variable before you run make.* * For example on my system librt is in /usr/lib/ so I would run in my shell $ export LLVM_LIB_SEARCH_PATH=/usr/lib* *But I did find LLVM-LD in my computer, because I downloaded the LLVM-3.4 with the order sudo apt-get install clang-3.4 llvm-3.4 llvm-3.4-dev llvm-3.4-tools. Also I did not found librt in my computer.* Thank you. Zhiyi Zhang
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev