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