[klee-dev] 回复： Some Question about Klee

[Kuchta, Tomasz]

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, 明白了 <1196467124 at qq.com<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"<t.kuchta at imperial.ac.uk<mailto:t.kuchta at imperial.ac.uk>>;
发送时间: 2013年4月13日(星期六) 凌晨0:00
收件人: "t.kuchta"<t.kuchta at imperial.ac.uk<mailto:t.kuchta at imperial.ac.uk>>;
抄送: "明白了"<1196467124 at qq.com<http://qq.com>>; "klee"<klee-dev at imperial.ac.uk<mailto:klee-dev at imperial.ac.uk>>;
主题: 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 at ubuntu:~/work/klee/examples/sort$
>> <mailto:bx at ubuntu:~/work/klee/examples/sort$> llvm-gcc -I ../../include
>> -c -g sort.c
>> bx at ubuntu:~/work/klee/examples/sort$
>> <mailto: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$
>> <mailto:bx at ubuntu:~/work/klee/examples/sort$> ls
>> sort.c sort.c~ sort.o
>> bx at ubuntu:~/work/klee/examples/sort$
>> <mailto: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
>>
>>
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk<mailto:klee-dev at imperial.ac.uk>
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
>
>



-------------- next part --------------
A non-text attachment was scrubbed...
Name: winmail.dat
Type: application/ms-tnef
Size: 9311 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20130413/cc071709/attachment.bin>