[klee-dev] klee_make_symbolic function definition

[Kuchta, Tomasz]

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 <leftcopy.chx at gmail.com<mailto: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
_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk<mailto:klee-dev at imperial.ac.uk>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: winmail.dat
Type: application/ms-tnef
Size: 5398 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20131031/7632bc4c/attachment.bin>