このホワイト ペーパーの図 7 の結果を再現するのに問題があります。
http://www.stanford.edu/~engler/klee-osdi-2008.pdf
具体的には、コア util の「tac」コマンドをテストしてみました。
klee.cde -max-time=60 --optimize --libc=uclibc --posix-runtime ./tac.bc -r -sym-files 20 1
ただし、紙にはバグがあるはずだと書かれていますが、KLEE から報告されたエラー メッセージは表示されません。
一方、core 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」コマンドのバグを発見するために、誰かが私を正しい方向に向けることができますか? どちらも、論文でそれぞれ「\b\b\b\b\b\b\b\t」および「\n」と定義されているファイル「t2.txt」および「t3.txt」が必要な場合です。
すべて/アドバイスをいただければ幸いです。