exponenta event banner

Изменение или отключение проверок времени выполнения программы проверки кода

При анализе средства проверки кода выполняется исчерпывающая проверка исходного кода на наличие распространенных ошибок во время выполнения. Исчерпывающий характер статического анализа предназначен для предотвращения возникновения ошибок во время выполнения критического программного обеспечения безопасности. Из-за критической цели анализа, связанной с безопасностью, программа Code Prover не позволяет:

  • Выборочно отключать определенные проверки времени выполнения.

  • Скрытие результатов проверок во время выполнения из списка результатов через аннотации исходного кода. Можно выровнять результаты с помощью аннотаций, но выровненные результаты будут по-прежнему отображаться в списке результатов.

Можно подавить определенные результаты, применив фильтры после анализа или даже создав отфильтрованные отчеты. При создании отфильтрованного отчета из результатов проверки кода в отчете отображаются фильтры и отражаются выбранные варианты. Дополнительные сведения см. в разделах Фильтрация и группирование результатов в интерфейсе пользователя Polyspace Desktop и Создание отчетов.

Однако можно изменить поведение некоторых проверок по умолчанию и полностью отключить их для инициализации. При создании отчета на основе результатов анализа отчет показывает использование этих опций.

В этом разделе перечислены параметры, изменяющие поведение по умолчанию определенных проверок времени выполнения. Следует отметить, что, хотя опция в основном относится к определенному типу проверки, она также влияет на проверки других типов. См. раздел Анализ проверки кода после проверки красного и оранжевого цветов.

Переполнение целого числа

ПроверитьПоведение по умолчаниюВыбор
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)

Инициализация

ПроверитьПоведение по умолчаниюВыбор

Проверки инициализации выполняются только при чтении переменной.

Disable checks for non-initialization (-disable-initialization-checks)

Global variable not assigned a value in initialization code

Проверка инициализации глобальной переменной выполняется только при считывании переменной.

Функции библиотеки

ПроверитьПоведение по умолчаниюВыбор
Invalid use of standard library routine

Только стандартные подпрограммы библиотеки проверяются на достоверность аргументов. Пользовательские библиотечные функции не проверяются.

-code-behavior-specifications

Указатели

ПроверитьПоведение по умолчаниюВыбор
Illegally dereferenced pointer

Указатели на поле структуры не могут указывать на другое поле.

Enable pointer arithmetic across fields (-allow-ptr-arith-on-struct)

Illegally dereferenced pointer

Указатели на структуру должны иметь достаточно буфера для всей структуры.

Allow incomplete or partial allocation of structures (-size-in-bytes)
Illegally dereferenced pointerОтмена привязки указателя стека за пределами области не обнаружена.Detect stack pointer dereference outside scope (-detect-pointer-escape)
Correctness conditionНесовпадения указателей функций недопустимы.Permissive function pointer calls (-permissive-function-pointer)

Недоступный код или мертвый код

КонтролерПоведение по умолчаниюВыбор

Незакрепленные функции и функции, вызываемые из недостижимого кода, не сообщаются.

Detect uncalled functions (-uncalled-function-checks)

Связанные темы