[klee-dev] Questions about getting symbolic execution tree with KLEE

[Chengyu Zhang]

Hi Zachery,
         Do you mean the symbolic execution tree?
         There is a data structure named PTree(ProcessTree) in KLEE, which
is generated during the symbolic execution process,  PTree Node will fork
when the corresponding State forks.
         The PTree contains some information of symbolic execution will be
useful for you.

         Here is another KLEE feature may be useful. I'm not sure if it
will work well.
         You can run KLEE with -write-paths (records both concrete an
symbolic path) or -write-sym-paths (just records symbolic path) options,
KLEE will write the binary sequences for each test case in the file named
"paths.ts" or "symPaths.ts" which indicates the branch chooses for each
case.
         Furthermore, there seems has a hack tool which could convert KLEE
treestream's of path branch information into images (
https://github.com/klee/klee/tree/master/utils/hacks/TreeGraphs).

         I hope it helps you.

Cheers
Chengyu

2017-12-29 13:18 GMT+08:00 Zachery <958919277 at qq.com>:

> Hi all,
>     Since KLEE is a tool of symbolic execution, is there a way to output
> the symbolic tree into a file?
>     I have searched for the solution both in klee-dev’s searchable archive
> <http://www.mail-archive.com/klee-dev@imperial.ac.uk/> and Google Search,
> but there seemed to be no answer.
>     So, could someone tell me how to get the symbolic tree or is there a
> tool for this task?
>
> Thanks in advance,
> Zachery
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>


-- 
张枨宇   Chengyu Zhang
East China Normal University
School of Computer Science and Software Engineering
Tel: +86 18685412181
Mail: dale.chengyu.zhang at gmail.com
-------------- next part --------------
HTML attachment scrubbed and removed