Во избежание недоказанности результатов (проверки оранжевого цвета) по причинам, не относящимся к коду, программа Code Prover предполагает, что определенные виды входных данных являются безопасными определенными способами. Например, указатели из внешних источников по умолчанию считаются ненулевыми. Чтобы просмотреть список допущений, которые можно вернуть с помощью параметров анализа, на панели Панель мониторинга в интерфейсе пользователя программы проверки кода выберите Просмотр предположений анализа для результатов. Чтобы перейти к параметру, изменяющему предположение, щелкните его правой кнопкой мыши.
Более полный список предположений см. здесь. Этот список показывает как разрешительные, так и консервативные допущения, сделанные в стандартном анализе проверки кода.
Почему при проверке в полиспейсе используются аппроксимации
Узнайте, как статическая проверка использует аппроксимации для выполнения превосходной проверки ошибок во время выполнения по сравнению с динамическими подходами.
Допущения о переменных диапазонах
Проверка использует тип данных внешней переменной для извлечения ее возможного диапазона значений.
Допущения относительно упорных функций
Верификация блокирует неопределенные функции или функции, которые необходимо блокировать, и делает определенные предположения относительно их аргументов и возвращаемых значений.
Допущения относительно основной функции
Проверка предполагает некоторые ограничения на main аргументы функции.
Допущения относительно инициализации глобальной переменной
Проверка предполагает инициализацию глобальных переменных по стандартам ANSI ® C, например, 0 дляint.
Допущения о изменчивых переменных
Проверка предполагает, что изменчивая переменная может принимать любое возможное значение в любой точке кода.
Допущения об определениях и объявлениях переменных и функций
Проверка демонстрирует различное поведение для незаявленных и неопределенных переменных или функций.
Допущения относительно стандартных процедур с плавающей запятой библиотеки
Для некоторых стандартных подпрограмм float библиотеки с двумя аргументами проверка может игнорировать аргументы функции и предполагать, что функция возвращает все возможные значения в своем диапазоне.
Проверка предполагает все возможные значения, если вы записываете на члена профсоюза, но читаете обратно другого члена того же профсоюза.
Допущения о переменных, приводимых в виде пустых указателей
Проверка теряет точность при приведении переменной к void* указатель.
Допущения об неявных преобразованиях типов данных
Проверка может предполагать неявное преобразование типа для двоичных операций в зависимости от типов данных операнда.
Допущения относительно memset и memcpy
Проверка выполняется только для определенных проблем при использовании memcpy и memsetи делает некоторые предположения после его использования.
Предположения о директивах # pragma
При проверке учитываются только определенные #pragma директивы, поскольку большинство таких директив не имеют отношения к проверке.
Допущения относительно кода сборки
Проверка распознает встроенные ассемблеры как вводящие сборочный код и игнорирует операции в сборочном коде.
Определение использования стека программ
Проверка оценивает использование стека из иерархии вызовов функции и размеров локальных переменных.
Ограничения проверки полиспейса
Просмотрите список подтвержденных ограничений проверки Polyspace ® в отношении определенных конструкций кода.