0

我正在尝试在 coreutils 的编译字节码版本上运行 klee,这在某种程度上复制了 klee 不久前所做的实验。

我在弄清楚如何使用 --max-time 标志时遇到了一些麻烦。

当我运行这个命令时,它需要大约 3 分钟,尽管最大时间是 10 秒:

klee --optimize --libc=uclibc --posix-runtime --max-time 10s ./echo.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdin 8 --sym-stdout

当我运行这个命令时,大约需要 3 秒。该命令是相同的,除了文件名和 --max-time 标志被切换的事实。

klee --optimize --libc=uclibc --posix-runtime --max-time 10s ./echo.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdin 8 --sym-stdout

最后,当我在没有 --max-time 标志的情况下运行它时

klee --optimize --libc=uclibc --posix-runtime ./echo.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdin 8 --sym-stdout

至少需要30分钟,此时我放弃并杀死了它。

显然,文件名前后的标志都在做某事,但我不确定是什么。根据文档, --max-time 的标准用法将其放在文件名之前。谁能帮我理解发生了什么?

4

1 回答 1

0

KLEE 使用 llvm 的命令行参数预处理器实现。由于InputFileoption 是一个位置参数,所有后面的参数都被忽略。但是,诸如 、 、 之类--sym-args--sym-files选项--sym-stdinPOSIX 运行时中独立处理。

于 2021-03-24T09:29:19.693 回答