Анализ Code Prover полностью проверяет исходный код на наличие распространенных ошибок времени выполнения. Исчерпывающий характер статического анализа предназначен для предотвращения возникновения ошибок во время выполнения в критическом программном обеспечении безопасности. Из-за критического намерения анализа безопасности Code Prover не позволяет:
Выборочно отключите определенные проверки во время выполнения.
Скрыть результаты проверок во время выполнения из списка результатов с помощью аннотаций исходного кода. Можно выровнять результаты с помощью аннотаций, но выровненные результаты продолжают отображаться в списке результатов.
Можно принять решение подавить определенные результаты путем применения фильтров после анализа или даже создания отфильтрованных отчетов. Если вы создаете отфильтрованный отчет из результатов Code Prover, отчет показывает фильтры и отражает выбранные вами варианты. Для получения дополнительной информации смотрите Фильтрация и группирование результатов в интерфейсе пользователя Polyspace Desktop и Генерация отчетов.
Однако можно изменить поведение некоторых проверок по умолчанию и полностью отключить проверки для инициализации. При создании отчета из результатов анализа в отчете показано использование этих опций.
В этом разделе перечислены опции, которые изменяют поведение по умолчанию некоторых проверок во время выполнения. Обратите внимание, что хотя опция в основном относится к определенному типу проверки, проверки других типов также затрагиваются. Смотрите Анализ Code Prover После красных и оранжевых проверок.
| Проверить | Поведение по умолчанию | Опция |
|---|---|---|
Invalid shift operations | Левые сдвиги не разрешены для подписанных операндов. | Allow negative operand for left shifts (-allow-negative-operand-in-shift) |
Overflow | Подписанные целочисленное переполнение запрещены. | Overflow mode for signed integer (-signed-integer-overflows) |
Overflow | Беззнаковое целочисленное переполнение не обнаружено. | Overflow mode for unsigned integer (-unsigned-integer-overflows) |
| Проверить | Поведение по умолчанию | Опция |
|---|---|---|
Неоконечные поплавки не рассматриваются. | ||
Subnormal float | Субнормальные результаты не обнаружены. | Subnormal detection mode (-check-subnormal) |
| Проверить | Поведение по умолчанию | Опция |
|---|---|---|
Проверки на инициализацию выполняются только при считывании переменной. |
| |
Global variable not assigned a value in initialization code | Проверки инициализации глобальной переменной выполняются только при считывании переменной. |
| Проверить | Поведение по умолчанию | Опция |
|---|---|---|
Invalid use of standard library routine | Только стандартные стандартные программы библиотеки проверяются на валидность аргументов. Пользовательские функции библиотеки не проверяются. | -code-behavior-specifications |
| Проверить | Поведение по умолчанию | Опция |
|---|---|---|
Illegally dereferenced pointer | Указатели на поле структуры не могут указывать на другое поле. |
|
Illegally dereferenced pointer | Указатели на структуру должны иметь достаточно буфера для всей структуры. | Allow incomplete or partial allocation of structures (-size-in-bytes) |
Illegally dereferenced pointer | Dereference указателя на стек вне возможностей не обнаружен. | Detect stack pointer dereference outside scope (-detect-pointer-escape) |
Correctness condition | Несоответствия указателя на функцию не допускаются. | Permissive function pointer calls (-permissive-function-pointer) |
| Контролер | Поведение по умолчанию | Опция |
|---|---|---|
О незакрытых функциях и функциях, вызываемых из недоступного кода, не сообщается. |
