[klee-dev] Path constraints as equations of integers

[Papapanagiotakis-Bousy, Iason]

Hello,

I am a new user of KLEE, I was looking into symbolic execution in order to extract the constraints of the input variables of a program for each path in the code.
Following the initial tutorials and searching on the web I've managed to get both the KQuery and SMT2 formatted constraints generated by KLEE.

I was wondering if there is a (new) capability of KLEE or an available script/tool to generate the constraints as a systems of equations of integers and not Bit Vectors as the default output in KQuery and SMT2 is.
While the output generated works fine with SMT solvers for the main purpose of KLEE, it would help a lot if constraints could also be presented in a human-friendly way.

This question has been asked in the past (2 years ago in this list) but I couldn't find any solution to this problem online.

Thank you in advance for letting me know if there is an existing solution to this.

Best regards,
Iason Papapanagiotakis
-------------- next part --------------
HTML attachment scrubbed and removed