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

[Cristian Cadar]

Hi Adam,

I think that would be a useful feature, that we considered in the past 
but never implemented.  Your plan sounds fine, although I'm not sure you 
really need an additional LLVM pass.  Also, the change should be 
backwards compatible (ktest files are already versioned).  But we can 
discuss all these details once you open a pull request on GitHub.

Best,
Cristian

On 30/03/18 22:17, Ádám Kubriczky wrote:
> 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
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>