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