Я пытаюсь запустить klee на скомпилированной версии coreutils с байт-кодом, несколько повторяя эксперимент, который 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 ставит его перед именем файла. Может ли кто-нибудь помочь мне понять, что происходит?
