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...@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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
