[klee-dev] Some Question about Klee

[明白了]

Sorry to interrupt you, but I really need some help in the problems I come across:
The first question is the following error:
bx at ubuntu:~/work/klee/examples/sort$ llvm-gcc -I ../../include -c -g sort.c
bx at ubuntu:~/work/klee/examples/sort$ klee sort.o
KLEE: ERROR: error loading program 'sort.o': Invalid bitcode signature
bx at ubuntu:~/work/klee/examples/sort$ ls
sort.c  sort.c~  sort.o
bx at ubuntu:~/work/klee/examples/sort$ klee --only-output-states-covering-new sort.o
KLEE: ERROR: error loading program 'sort.o': Invalid bitcode signature
When compiling the file sort.c in the example category of klee, it generates file sort.o. But when the file sort.o isn’t used, it will report this error, saying it’s an invalid bitcode signature. I can’t figure out what’s wrong with this.
 
The second question is :
We installs the system 12.04 version of klee according to the installing steps that you publish on the web, but it reports the error above when compiling, saying it is a “unrecognized option ‘--emit-llvm’”. Why was it so? I need some help in this.

And the last question is that, how to test the whole project together instead of testing the files one by one? What’s more, the examples you give are all involved with a function klee_make_symblic which is used in the main function. This function has a parameter that is the variable of the function to be tested. Do you just provide testing examples that are only involved the paths which are related to this variable?
Thank you for taking time to read these. I am hoping for your reply.
Thank you very much.
Yours sincerely,
Paul
-------------- next part --------------
HTML attachment scrubbed and removed