[klee-dev] Interpreting the output of --write-sym-paths and --write-paths

Cristian Cadar c.cadar at imperial.ac.uk
Tue Jan 10 22:39:57 GMT 2017


Hi Sean, the .path files are recording the branches followed by the 
paths explored by KLEE -- one could also replay them later on if needed. 
  But this feature needs more work to be usable, and we've started 
fixing it a few months ago, but haven't finished it yet.

The other feature was added by Daniel a long time ago to visualize KLEE 
paths, but I'm not sure if it still works.  If you're successful 
reviving it, it would be great if you could contribute some 
documentation to the website about it.

Best,
Cristian

On 09/01/2017 12:45, Sean Heelan wrote:
> Hi,
>
> I was wondering if someone could enlighten me as to how the paths.ts,
> symPaths.ts, test*.path and test*.sym.path files generated by
> --write-sym-paths and --write-paths can be used?
>
> Some googling turned up [1] but, other than that, is there an intended
> application for processing this data?
>
> Cheers,
> Sean
>
> [1] https://gitlab.doc.ic.ac.uk/dsl11/klee-cl/tree/two_thread_hack/utils/hacks/TreeGraphs
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>



More information about the klee-dev mailing list