Пример игрушки CBMC

Question

Я новичок в CBMC и экспериментирую с ним. В этой связи здесь есть пример игрушки для проверки функции binsearch с СВМСОМ. Я решил запустить следующую команду, которую они предоставили, просто изменив количество раз, когда цикл разматывался:

      cbmc binsearch.c --function binsearch --unwind 4 --bounds-check --unwinding-assertions

Он вернул следующее:

      ** Results:
[binsearch.unwind.0] unwinding assertion loop 0: FAILURE
prog.c function binsearch
[binsearch.array_bounds.1] line 7 array `a' lower bound in a[(signed long int)middle]: SUCCESS
[binsearch.array_bounds.2] line 7 array `a' upper bound in a[(signed long int)middle]: SUCCESS
[binsearch.array_bounds.3] line 9 array `a' lower bound in a[(signed long int)middle]: SUCCESS
[binsearch.array_bounds.4] line 9 array `a' upper bound in a[(signed long int)middle]: SUCCESS

Является ли плохим тот факт, что утверждение раскручивания не удалось из-за недостаточного количества итераций? С моей точки зрения, похоже, что в этом примере нет ошибок, потому что код не обращался к тем частям памяти, которые ему не должны были быть доступны, но я не уверен, основываясь на этом сбое одного утверждения при раскручивании. У кого-нибудь есть идеи по поводу безопасности? Имеет ли значение эта неудача?

Answer 1

На основе свойство, которое проверяет следующее:

Проверяет, достаточно велик, чтобы покрыть все пути программы. Если аргумент слишком мал, CBMC обнаружит, что выполнено недостаточно раскручивания, и сообщит, что утверждение раскручивания не удалось.

Я бы сказал, что это предупреждение о возможности недостаточного количества итераций цикла, чтобы убедиться, что функция не получит доступ к массиву за пределами границ. Это означает, что хотя функция не нарушила никаких свойств с 4, нам нужно проверить все пути, прежде чем мы сможем сказать, что это безопасно.