回复： 回复： 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-***@public.gmane.org<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-AQ/***@public.gmane.org<mailto:t.kuchta12-AQ/***@public.gmane.org>>;
·¢ËÍʱŒä: 2013Äê4ÔÂ21ÈÕ(ÐÇÆÚÌì) ÍíÉÏ6:34
ÊÕŒþÈË: "Ã÷°×ÁË"<1196467124-***@public.gmane.org<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-***@public.gmane.org<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-AQ/***@public.gmane.org<mailto:***@imperial.ac.uk>>;
·¢ËÍʱŒä: 2013Äê4ÔÂ13ÈÕ(ÐÇÆÚÁù) Á賿0:00
ÊÕŒþÈË: "t.kuchta"<t.kuchta-AQ/***@public.gmane.org<mailto:***@imperial.ac.uk>>;
³­ËÍ: "Ã÷°×ÁË"<1196467124-***@public.gmane.org<http://qq.com/>>; "klee"<klee-dev-AQ/***@public.gmane.org<mailto:klee-dev-AQ/***@public.gmane.org>>;
Ö÷Ìâ: Re: [klee-dev] Some Question about Klee

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

Sorry to interrupt you, but I really need some help in the problems I
-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