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 <[email protected]>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 <[email protected]> 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 >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
