Thank you, Christian. I am new to KLEE, I have a lot simple questions.
How does KLEE handle structure, unsigned int, long types?
For example,
struct A {unsigned int a, short int b};
main()
{
A obj_A;
klee_make_symbolic (&obj_A, sizeof(obj_A), "obj"); // can I do
this?
}
As for int, does a = klee_int ("newint"); works equivalent to int a;
klee_make_symbolic(&a, sizeof(int), "newint") ?
Thanks,
Xiao
Cristian Cadar <c.cadar at imperial.ac.uk>
09/27/2010 06:34 PM
To
Xiao Qu/USABB/ABB at ABB
cc
"klee-dev at keeda.stanford.edu" <klee-dev at keeda.stanford.edu>
Subject
Re: [klee-dev] klee replay and coverage information
Hi Xiao,
> 1. In the tutorials, only klee_make_symbolic_name and klee_make_symbolic
> are used, where can I find the other methods such as "klee_int" you
> mentioned? Any documentation on how to use these methods?
You can find the entire list of KLEE intrinsics, with comments, in
include/klee/klee.h.
> 2. In the second case where I use "KTEST_FILE=xxx; ./a.out;" for replay,
> gcov will also count the codes in /Release/lib/ ---- maybe in these
> cases, we need to manually run test cases in order to get "pure"
coverage.
You should be able to simply ignore that directory when you aggregate
coverage information.
Best,
Cristian
> Thanks,
> Xiao
>
>
>
>
> *Wujie Zheng <wjzheng at cse.cuhk.edu.hk>*
>
> 09/27/2010 01:12 PM
>
>
> To
> Xiao Qu/USABB/ABB at ABB
> cc
> klee-dev at keeda.stanford.edu
> Subject
> Re: [klee-dev] klee replay and coverage information
>
>
>
>
>
>
>
>
> Hi Xiao
>
> 1. If you use only symbolic arguments, use "klee-replay ./a.out
> klee-last/*.ktest;" (a.out is the program under test compiled normally)
> If you use klee_int or other methods, use "KTEST_FILE=xxx; ./a.out;"
> (a.out needs to be compiled with the libraries under /Release/lib/)
> 2. I don't check the info in run.stats carefully, but it is convenient
> to use gcov to collect the coverage information. You can write a simple
> parser for the .gcov files. For overall coverage of files in a
> directory, you can use the zcov tool.
>
> Best wishes,
> Wujie
>
> Xiao Qu wrote:
> >
> > Hi,
> >
> > I have some questions on replaying test cases and collecting coverage
> > information.
> >
> > 1. In Tutorial One and Three, there are two different methods to
> > replay test cases. One is build with "libkleeRuntest library" while
> > the other one is use "klee-replay" directly.
> >
> > I guess klee-replay only applies when the symbolic input is the
> > "direct" input parameters for the main function?
> >
> > Plus, I didn't find libkleeRuntest.dylib in Release/lib ?
> >
> >
> > 2. In order to collect coverage information, do I have to use gcov?
> > Can we just get the similar information from "*run.stats* " ?
> >
> > Thanks,
> > Xiao
> >
------------------------------------------------------------------------
> >
> > _______________________________________________
> > klee-dev mailing list
> > klee-dev at keeda.stanford.edu
> > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
> >
>
> <http://keeda.stanford.edu/mailman/listinfo/klee-dev>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100929/e57d2142/attachment.html
