Hi,
We are working on a security project, for which we modify KLEE to
build our tool.
We figured out that we need to print the expressions in SMT2 format. In
particular,
we intercept each load and store instruction, and we build queries on
the address
being read from or written to. These addresses might be symbolic and we
need to
print all these intermediate queries in SMT2 format. Is there a suitable
way to do this?
We figured out that ExprPPrinter class prints these expressions,
but, it seems
they only print in the interim .pc format. Is there a way to modify this
class to print
them in smt2 format directly?
Regards,
Sudipta
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
