Discussion:
Some Question about Klee
明白了
2013-04-12 15:11:02 UTC
Permalink
Sorry to interrupt you, but I really need some help in the problems I come across:
The first question is the following error:
***@ubuntu:~/work/klee/examples/sort$ llvm-gcc -I ../../include -c -g sort.c
***@ubuntu:~/work/klee/examples/sort$ klee sort.o
KLEE: ERROR: error loading program 'sort.o': Invalid bitcode signature
***@ubuntu:~/work/klee/examples/sort$ ls
sort.c sort.c~ sort.o
***@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
Tomasz Kuchta
2013-04-12 16:00:08 UTC
Permalink
Adding the list ..
Hi Paul,
Regarding your first question - try compiling with --emit-llvm option.
If compiler returns errors about c99 mode, you may want to try -std=c99
option as well.
Best Regards,
Tomek
Post by 明白了
-c -g sort.c
KLEE: ERROR: error loading program 'sort.o': Invalid bitcode signature
sort.c sort.c~ sort.o
--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.
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
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Jonathan Neuschäfer
2013-04-13 20:42:00 UTC
Permalink
Post by 明白了
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.
Try "-emit-llvm" (with only one leading dash), it worked for me
(llvm-gcc 4.6.3).

HTH,
Jonathan Neuschäfer
Hongxu Chen
2013-04-14 01:20:34 UTC
Permalink
AFAIK, the deb package of llvm-gcc is actually a dragonegg, you can see
what's happening by using

cat $(which llvm-gcc)

or sometihing like that.
Post by Jonathan Neuschäfer
Post by 明白了
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.
Try "-emit-llvm" (with only one leading dash), it worked for me
(llvm-gcc 4.6.3).
HTH,
Jonathan Neuschäfer
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
--
Regards,
Hongxu Chen
Jonathan Neuschäfer
2013-04-14 09:32:47 UTC
Permalink
Post by Hongxu Chen
AFAIK, the deb package of llvm-gcc is actually a dragonegg, you can see
what's happening by using
cat $(which llvm-gcc)
or sometihing like that.
Indeed. Thanks for pointing that out.


Jonathan Neuschäfer

Loading...