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