У меня возникли проблемы, воспроизводящий результат на рисунке 7 настоящей статьи:Каковы исходные данные для эксперимента KLEE core-utils, обсуждаемого в статье?
http://www.stanford.edu/~engler/klee-osdi-2008.pdf
В частности, я попытался проверить команду «нолики» на главном UTIL в этом:
klee.cde -max-time=60 --optimize --libc=uclibc --posix-runtime ./tac.bc -r -sym-files 20 1
Однако Я не вижу сообщений об ошибках, сообщенных KLEE, хотя бумага утверждает, что должна быть ошибка.
С другой стороны, если я испытываю «md5sum» ядро UTIL в команду, как так:
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), что, по-видимому, является довольно полным объяснением работы coreutils с klee. – kccqzy
[Здесь] (http://klee.llvm.org/CoreutilsExperiments.html) - другая страница с более подробной информацией. Похоже, они использовали намного более длинные варианты командной строки. – kccqzy