本文討論的KLEE core-utils實驗的輸入是什麼？

-1

具體而言，我試圖測試核心UTIL的「TAC」命令這樣做：

klee.cde -max-time=60 --optimize --libc=uclibc --posix-runtime ./tac.bc -r -sym-files 20 1

然而我沒有看到KLEE報告的任何錯誤消息，儘管文章聲稱應該有一個錯誤。

在另一方面，如果我考覈心UTIL的「的md5sum」命令，像這樣：

klee.cde -max-time=60 --optimize --libc=uclibc --posix-runtime ./md5sum.bc -c -sym-files 1 10

KLEE報告以下錯誤：

: /root/coreutils-6.10/obj-llvm/src/../../src/md5sum.c:212: memory error: out of bound pointer

有人可以點我在正確的方向發現「tac」或「pr」命令中的錯誤？如果這兩個文件分別需要文件「t2.txt」和「t3.txt」，它們分別定義爲「\ b \ b \ b \ b \ b \ b \ b \ t」和「\ n」。

希望所有/任何意見。

也許你可以看一下[本頁]（http://klee.llvm.org/TestingCoreutils.html），這似乎是一個用klee運行coreutils的非常完整的解釋。 – kccqzy

[這裏]（http://klee.llvm.org/CoreutilsExperiments.html）是另一個頁面，有更多的細節。看起來他們使用了更長的命令行選項。 – kccqzy

您可以嘗試使用較大的值--max-time，該值設置KLEE的時間限制。

2012-11-14 05:14:50 bwzhou

回答