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