[klee-dev] klee_make_symbolic function definition

[Hongxu Chen]

Thanks so much Daniel and Kuchta. Now I know what I was wrong about and
following Kuchta's advice I got the symbolic value name.

Best Regards,
Hongxu Chen




On Thu, Oct 31, 2013 at 5:02 PM, Daniel Liew <daniel.liew at imperial.ac.uk>wrote:

> KLEE will not let you call printf on symbolic data (I am not sure
> about fprintf). To check if something is symbolic you should use the
> klee_is_symbolic() (
> https://github.com/ccadar/klee/blob/master/include/klee/klee.h ).
>
> Also the implementation of klee_make_symbolic you link to is not what
> is used during symbolic execution. What you link to is the version of
> klee_make_symbolic used for replay. The version of klee_make_symbolic
> used during symbolic execution is in SpecialFunctionHandler.cpp ( see
>
> https://github.com/ccadar/klee/blob/master/lib/Core/SpecialFunctionHandler.cpp#L648
> )
>
> You can also use klee_print_expr("The value is:", your_expr); where
> your_expr can be pretty much anything.
>
> Hope that helps.
>
> On 31 October 2013 08:17, Hongxu Chen <leftcopy.chx at gmail.com> wrote:
> > Hi,
> >
> >    I hope to get to know what value is made symbolic during klee
> execution;
> > I add a printf log at the beginning of the function klee_make_symbolic
> > inside
> > runtime/Runtest/intrinsics.c(
> https://github.com/ccadar/klee/blob/master/runtime/Runtest/intrinsics.c#L34
> ):
> >
> > fprintf(stderr, "klee_make_symbolic for %s with %lu bytes\n", name,
> nbytes);
> >
> > However when running there is no output about it when klee meets
> > klee_make_symbolic function call in LLVM IR. So am I missing something?
> >
> > Best Regards,
> > Hongxu Chen
>
-------------- next part --------------
HTML attachment scrubbed and removed