[klee-dev] [KLEE-dev] printing queries in SMT2 format

sudiptac sudipta.chattopadhyay at liu.se
Tue Mar 31 13:46:51 BST 2015


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



More information about the klee-dev mailing list