[klee-dev] How to get the content of a symbolic variable?

General Email general_mail2011 at yahoo.com
Mon Apr 8 22:47:35 BST 2013


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
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list