Replies: 7 comments 3 replies
-
|
Мои рекомендации к обсуждению в четверг:
|
Beta Was this translation helpful? Give feedback.
-
|
Все .bc запускались с TL 180 секунд, если не указано иначе |
Beta Was this translation helpful? Give feedback.
-
|
Потенциальная проблема: куди считает, что глобальные объекты могут меняться всегда, поэтому klee нужно запускать с опцией |
Beta Was this translation helpful? Give feedback.
-
|
Иногда калькулятор расстояний не может понять, что из блока не достигается таргет, потому что в блоке есть инструкция вида |
Beta Was this translation helpful? Give feedback.
-
|
На а наш код в |
Beta Was this translation helpful? Give feedback.
-
|
дефолтный |
Beta Was this translation helpful? Give feedback.
-
|
Репозиторий со скриптами и результатами здесь |
Beta Was this translation helpful? Give feedback.
Uh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
-
Работа завершена, итоги:
void alloc*(void **ptr)как nop, поэтому значение указателя не меняется и всегда попадаем в ветку, где*ptr == NULL, из-за чего не доходим даже до первого таргетаRETURN_NULL_IF_NOT_OK_FOR_GROUPскрывает if иreturn NULL, и мы не можем понять, что event из трассы указывает на return, и проходим мимо.dplwt_estack_malloc, который возвращает символьный указатель. На него делаетсяmemsetна 184 байта, после которого получаетсяUseAfterFreeи стейт отрубается. Если поставить--min-number-elements-li=190и TL 1200, то исполнение всё-таки проходит дальшеmemset. От вызоваmemsetдоretиз него прошло 354235 миллисекунд. Если поставить--max-sym-alloc=2048 --min-number-elements-li=4 --use-sym-size-li=true, то это занимает 318256 миллисекунд._setjmpне поддержан в KLEEBeta Was this translation helpful? Give feedback.
All reactions