[klee-dev] making the ktest-tool's output more readable

[Ádám Kubriczky]

 Hello,

It would be very useful (for practical usage) to extend the ktest-tool's
functionality to provide readable output automatically at least for basic
integral types, arrays and structures composed of these types.

I’m planning to implement this feature and I would like to ask your opinion
about my proposed approach, or if you already had some better ideas on this
problem.

My planned solution is supposed to work without the use of any additional
tools (additional = not already used in the core of klee).

The plan: before any LLVM passes there would be an additional pass that
gains the necessary type informations about the symbolic variables and
outputs these meta information next to the .ktest files. With the use of
these, the ktest-tool could know how to show them (at least the most common
ones), and type-dependent formatting could be added to ktest-tool.

Thanks for your answer!

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