How to get the content of a symbolic variable?

Paul Marinescu

2013-04-09 13:00:42 UTC

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

Post by General Email
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev