You're probably looking for klee_print_expr, e.g. klee_print_expr("k = ", k)

You can include includes/klee/klee.h for the prototype.

Paul

On 08/04/13 22:47, General Email wrote:
Hi,

How to get the content of a symbolic variable?

When I tried to run the code listed below, I got the following output
from klee

KLEE: WARNING ONCE: calling external: printf(182324664, 182337984, (Add
w32 7 (ReadLSB w32 0 inVar)))
KLEE: ERROR: /home/try1.c:53: failed external call: printf

////////////////////////////////////////////////////////////////////////////////////////////////
int inVar;
klee_make_symbolic(&inVar, sizeof(inVar), "inVar");

int k = inVar+5;
k=k+2;
if (k>0)
{
     doBlock1;
}
else
{
     doBlock2;
}

printf("%s%s\n", "k = ", k);
///////////////////////////////////////////////////////////////////////////////////////////////////


I'm interested in getting the value presented in the last agrument of
the printf function which is :"(Add w32 7 (ReadLSB w32 0 inVar))".

Would you please tell me how to get this expression?
Thanks





_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev



_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Reply via email to