Я нахожусь в своем док-контейнере, исследуя игрушечную программу "get_sign.c", с которой поставляется KLEE. Я хочу исследовать различные пути символьного вычисления, выполняемого, когда я делаю:
clang -I ../../include -emit-llvm -c -g get_sign.c
Я вижу значения, которые символический калькулятор подключил через:
ktest-tool --write-ints klee-last/test*.ktest
Однако теперь я также хотел бы видеть фактические пути, если есть такая опция, или, по крайней мере, я хотел бы видеть условия пути, соответствующие каждому пути. Наконец, я хочу иметь возможность увидеть самый длинный / самый короткий путь и исследовать условия его пути.
Я ищу в каталоге klee-last и просматриваю эти файлы, но не вижу какой-либо явной информации об условиях пути в этих файлах и сообщениях .txt, если только я не распознаю их.