On 09/29/2010 03:43 PM, xiao.qu at us.abb.com wrote:
>
> 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?*
Yes, you can mark any memory object as symbolic (note that there are
some syntactical errors in your code though).
> }
>
>
> As for *int*, does * a = klee_int ("newint"); * works equivalent to *int
> a; klee_make_symbolic(&a, sizeof(int), "newint") *?
Yes.
Best,
Cristian
>
> 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>http://keeda.stanford.edu/mailman/listinfo/klee-dev>
>
