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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
