I am in my dock container exploring the toy "get_sign.c" program that KLEE comes with. I want to explore the different paths of the symbolic calculation executed when I do:
clang -I ../../include -emit-llvm -c -g get_sign.c
I can see the values the symbolic calculator plugged in via:
ktest-tool --write-ints klee-last/test*.ktest
However now I would also like to see the actual paths, if there is such an option, or at least I'd like to see the Path conditions corresponding to each path. Finally, I want to be able to see what is the longest/shortest path and explore their path conditions.
I am searching around the klee-last directory and viewing those files, but I don't see any explicit information about path conditions in those .txt files and messages, unless I am and I'm not recognizing them.
