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

[Kuchta, Tomasz]

Hello,

I know that it runs under Linux and also heard about MacOs (however I do not know current status) and they are both Unix based.
I am not sure - maybe someone on the list will know.

Best Regards,

Tomek


On 25 Apr 2013, at 06:38, 明白了 <1196467124 at qq.com<http://qq.com>> wrote:

can you tell me if the C project based on Windows can be analyzed by KLEE?
Thank you!



------------------ 原始邮件 ------------------
发件人: "Kuchta, Tomasz"<t.kuchta12 at imperial.ac.uk<mailto:t.kuchta12 at imperial.ac.uk>>;
发送时间: 2013年4月21日(星期天) 晚上6:34
收件人: "明白了"<1196467124 at qq.com<http://qq.com>>;
主题: Re: 回复： [klee-dev] Some Question about Klee

Hi Paul,

I'm sorry - unfortunately I do not know the response.

Best Regards,

Tomek

On 21 Apr 2013, at 09:33, 明白了 <1196467124 at qq.com<http://qq.com/>> wrote:

Hello:
I want to know How does Klee deal with the loop in the target code? In which part of the source code of Klee is corresponding with it?
Thanks a lot!



------------------ 原始邮件 ------------------
发件人: "t.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: 9822 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20130425/ced28825/attachment.bin>