本文讨论的KLEE core-utils实验的输入是什么？

问题描述：

具体而言，我试图测试核心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的时间限制。