[klee-dev] Getting symbolic expressions with their context

[Hooman Asadian]

Hello,

I've repurposed the 'klee_print_expr' function based on a previous 
discussion in the mailing list to print symbolic expressions in SMTLIB 
format. Currently, I use the following to output these expressions:

printer.printExpression(arguments[1], ExprSMTLIBPrinter::SORT_BITVECTOR);

My question is, how can I retrieve the context for variables that appear 
in these symbolic expressions? For example, I have the following 
symbolic expression:

recordSequenceNumber: (bvor (bvshl ((_ zero_extend 56) (select 
sequencenumber (_ bv0 32))) (_ bv40 64))
(bvor (bvshl ((_ zero_extend 56) (select sequencenumber (_ bv1 32))) (_ 
bv32 64))
(bvor (bvshl ((_ zero_extend 56) ?B3) (_ bv24 64)) (_ bv16777215 64))))

I can get the definition of |sequencenumber| from the path condition 
file (*.smt2), but |B3| is not something I made symbolic. It seems to be 
defined within the path condition. How can I retrieve its definition or 
better understand its origin?

Best,
Hooman Asadian
-------------- next part --------------
HTML attachment scrubbed and removed