[klee-dev] Path constraints as equations of integers

[Andrew Santosa]

Dear Iason,
I think a possible solution might be to modify ExprPPrinter class, such that KQuery format would instead displaythe constraints in the format that you want.

Best,
Andrew
 

    On Tuesday, 1 November 2016, 22:28, "Papapanagiotakis-Bousy, Iason" <iason.papapanagiotakis-bousy.15 at ucl.ac.uk> wrote:
 

  <!--#yiv5913723195 _filtered #yiv5913723195 {font-family:"Cambria Math";panose-1:2 4 5 3 5 4 6 3 2 4;} _filtered #yiv5913723195 {font-family:Calibri;panose-1:2 15 5 2 2 2 4 3 2 4;}#yiv5913723195 #yiv5913723195 p.yiv5913723195MsoNormal, #yiv5913723195 li.yiv5913723195MsoNormal, #yiv5913723195 div.yiv5913723195MsoNormal {margin:0cm;margin-bottom:.0001pt;font-size:11.0pt;font-family:"Calibri", sans-serif;}#yiv5913723195 a:link, #yiv5913723195 span.yiv5913723195MsoHyperlink {color:#0563C1;text-decoration:underline;}#yiv5913723195 a:visited, #yiv5913723195 span.yiv5913723195MsoHyperlinkFollowed {color:#954F72;text-decoration:underline;}#yiv5913723195 p.yiv5913723195msonormal0, #yiv5913723195 li.yiv5913723195msonormal0, #yiv5913723195 div.yiv5913723195msonormal0 {margin-right:0cm;margin-left:0cm;font-size:12.0pt;font-family:"Times New Roman", serif;}#yiv5913723195 span.yiv5913723195EmailStyle18 {font-family:"Calibri", sans-serif;color:windowtext;}#yiv5913723195 span.yiv5913723195EmailStyle19 {font-family:"Calibri", sans-serif;color:windowtext;}#yiv5913723195 .yiv5913723195MsoChpDefault {font-size:10.0pt;} _filtered #yiv5913723195 {margin:72.0pt 90.0pt 72.0pt 90.0pt;}#yiv5913723195 div.yiv5913723195WordSection1 {}-->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 
_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


   
-------------- next part --------------
HTML attachment scrubbed and removed