Hello, You could try to do the following to print the name of the symbolic variable:
In lib/Core/SpecialFunctionHanlder.cpp there is a handler named handleMakeSymbolic. At the beginning of the handler, there is an if-else block and in the ‘else’ part ‘name’ string is set. You could try to add klee_message(“symbolic variable name: %s”, name.c_str()); to print the name string. Hope that helps, Best regards, Tomek On 31 Oct 2013, at 08:17, Hongxu Chen <[email protected]<mailto:[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]<mailto:[email protected]> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
<<attachment: winmail.dat>>
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
