- 文獻(xiàn)標(biāo)題： Overview of the main files generated by KLEE
- 文獻(xiàn)作者： The KLEE Team.
- 文獻(xiàn)來(lái)源： http://klee.github.io/docs/files/
- 閱讀日期： 2015年12月23日22時(shí)許
- 閱讀程度： 速讀
標(biāo)準(zhǔn)全局文件
-
info： 包含了與KLEE運(yùn)行相關(guān)的各類(lèi)信息的文本文件，例如：
$ cat info
klee --write-pcs demo.o
PID: 12460
Started: 2009-05-20 22:31:41
BEGIN searcher description
DFSSearcher
END searcher description
Finished: 2009-05-20 22:31:41
Elapsed: 00:00:00
KLEE: done: explored paths = 3
KLEE: done: avg. constructs per query = 6
KLEE: done: total queries = 3
KLEE: done: valid queries = 0
KLEE: done: invalid queriers = 3
KLEE: done: query cex = 3
KLEE: done: total instructions = 67
KLEE: done: completed paths = 3
KLEE: done: generated tests = 3 - warnings.txt： 包含了KLEE生成的所有警告信息的文本文件沛励。
- messages.txt： 包含了KLEE生成的所有消息的文本文件张抄。
- assembly.ll： 包含了被KLEE執(zhí)行的可讀樣式的LLVM bitcode纤怒。
- run.stats： 包含了KLEE生成的各式統(tǒng)計(jì)信息的文本文件芦昔，可以用klee-stats工具解析它栽惶。
- run.istats： 包含KLEE生成的程序中每行代碼對(duì)應(yīng)的全局統(tǒng)計(jì)信息的二進(jìn)制文件。
其他全局文件
- all-queries.pc： KLEE在KQuery模式下執(zhí)行的所有查詢(xún)芍殖。這些是優(yōu)化之前的查詢(xún)豪嗽，所以有些記錄的查詢(xún)可能根本沒(méi)被KLEE求解器修改或執(zhí)行。文件輸出開(kāi)關(guān)為：--use-query-log=all:pc to KLEE.
- all-queries.smt2： 包含在SMT-LIBv2中的執(zhí)行的KLEE查詢(xún)豌骏。包含的信息同文件all-queries.pc.開(kāi)關(guān)參數(shù)為： --use-query-log=all:smt2 to KLEE.
- solver-queries.pc： 包含KQuery格式下所有傳遞給KLEE求解器的查詢(xún)龟梦，這些查詢(xún)是優(yōu)化后的。開(kāi)關(guān)參數(shù)為：--use-query-log=solver:pc to KLEE.
- solver-queries.smt2： 包含SMT-LIBv2格式下所有傳遞給KLEE求解器的查詢(xún)窃躲，這些查詢(xún)是優(yōu)化后的计贰。包含的信息同文件solver-queries.pc。開(kāi)關(guān)參數(shù)為：--use-query-log=solver:smt2 to KLEE.
路徑相關(guān)文件
- test<N>.ktest： KLEE生成的能觸發(fā)該路徑的測(cè)試樣本蒂窒，要用ktest-tool處理該文件躁倒。可以用 --no-output 參數(shù)關(guān)閉此文件的生成刘绣。
- test<N>.<error-type>.err： 當(dāng)KLEE在觸發(fā)路徑時(shí)出錯(cuò)樱溉，生成此文件，包含了文本樣式的錯(cuò)誤信息纬凤。
- test<N>.pc： 以KQuery格式存儲(chǔ)與該路徑相關(guān)的約束。通過(guò) --write-pcs 開(kāi)關(guān)生成此類(lèi)文件撩嚼。
- test<N>.cvc： 以CVC格式存儲(chǔ)與該路徑相關(guān)的約束停士。通過(guò) --write-cvcs 開(kāi)關(guān)生成此類(lèi)文件。
- test<N>.smt2： 以SMT-LIBv2格式存儲(chǔ)與該路徑相關(guān)的約束完丽。通過(guò) --write-smt2s 開(kāi)關(guān)生成此類(lèi)文件恋技。
