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

[Paul Marinescu]

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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>