[klee-dev] klee_make_symbolic function definition

Hongxu Chen leftcopy.chx at gmail.com
Thu Oct 31 08:17:59 GMT 2013


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


More information about the klee-dev mailing list