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