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
