Анализ Программы автоматического доказательства Кода исчерпывающе проверяет исходный код на общие ошибки времени выполнения. Исчерпывающая природа статического анализа спроектирована, чтобы препятствовать ошибкам произойти во время выполнения в безопасности критическое программное обеспечение. Из-за безопасности критическое намерение анализа Программа автоматического доказательства Кода не позволяет вам:
Выборочно отключите определенные проверки на этапе выполнения.
Скройте результаты проверок на этапе выполнения от списка результатов до аннотаций исходного кода. Можно выровнять по ширине результаты через аннотации, но выровненные по ширине результаты продолжают появляться в списке результатов.
Можно принять решение подавить определенные результаты путем применения фильтров после анализа или даже создания отфильтрованных отчетов. Если вы создаете отфильтрованный отчет из результатов Программы автоматического доказательства Кода, отчет показывает фильтры и отражает ваш выбор. Для получения дополнительной информации смотрите Результаты Фильтра и Группы в Пользовательском интерфейсе Рабочего стола Polyspace и Сгенерируйте Отчеты.
Однако можно изменить поведение по умолчанию определенных проверок и полностью отключить проверки на инициализацию. Когда вы генерируете отчет от результатов анализа, отчет показывает использование этих опций.
Эта тема перечисляет опции, которые изменяют поведение по умолчанию определенных проверок на этапе выполнения. Обратите внимание на то, что, хотя опция, в основном, обращается к определенному типу проверки, на проверки других типов также влияют. Смотрите, что Анализ Программы автоматического доказательства Кода Следует за Красными и Оранжевыми Проверками.
| Проверять | Поведение по умолчанию | Опция |
|---|---|---|
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 | Указатель вершины стека разыменовывает внешний осциллограф, не обнаруживается. | Detect stack pointer dereference outside scope (-detect-pointer-escape) |
Correctness condition | Несоответствия указателя функции не позволены. | Permissive function pointer calls (-permissive-function-pointer) |
| Средство проверки | Поведение по умолчанию | Опция |
|---|---|---|
О невостребованных функциях и функциях, вызванных из недостижимого кода, не сообщают. |
