我正在尝试在 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 的标准用法将其放在文件名之前。谁能帮我理解发生了什么?