Hi Paul, Yes, klee is able to tell that for example buffer overflow occurred on a given line in a given file, so the location of the error is reported to the user.
I don't know however how exactly this information is extracted internally by klee, i.e. whether it is stored in LLVM bitcode or extracted in some other way. Best Regards, Tomek On 13 Apr 2013, at 18:30, ?????? <[email protected]<http://qq.com>> wrote: Sorry for interrupting you again. But I am still confused with some problems: The first one is that if the .o file generated by llvm records the information of the source file? If it doesn't, how can you make sure the location of the code that generate bugs? Besides, you have mentioned in your essays that there exists klee which can be used to test the bugs in the code, so could you locate exactly which part of the code that causes the bugs? Thank you very much for your reply. I appreciate it a lot. I am looking forward to your help. Yours sincerely, Paul ------------------ ???????? ------------------ ??????: "Tomasz Kuchta"<[email protected]<mailto:[email protected]>>; ????????: 2013??4??13??(??????) ????0:00 ??????: "t.kuchta"<[email protected]<mailto:[email protected]>>; ????: "??????"<[email protected]<http://qq.com>>; "klee"<[email protected]<mailto:[email protected]>>; ????: Re: [klee-dev] Some Question about Klee Adding the list .. On 12/04/13 16:59, Tomasz Kuchta wrote: > 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 > > On 12/04/13 16:11, ?????? wrote: >> Sorry to interrupt you, but I really need some help in the problems I >> come across: >> The first question is the following error: >> bx@ubuntu:~/work/klee/examples/sort$ >> <mailto:bx@ubuntu:~/work/klee/examples/sort$> llvm-gcc -I ../../include >> -c -g sort.c >> bx@ubuntu:~/work/klee/examples/sort$ >> <mailto:bx@ubuntu:~/work/klee/examples/sort$> klee sort.o >> KLEE: ERROR: error loading program 'sort.o': Invalid bitcode signature >> bx@ubuntu:~/work/klee/examples/sort$ >> <mailto:bx@ubuntu:~/work/klee/examples/sort$> ls >> sort.c sort.c~ sort.o >> bx@ubuntu:~/work/klee/examples/sort$ >> <mailto:bx@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 >> >> >> >> _______________________________________________ >> klee-dev mailing list >> [email protected]<mailto:[email protected]> >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> > >
<<attachment: winmail.dat>>
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
