[klee-dev] klee_make_symbolic function definition

[Daniel Liew]

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