Exponenta Banner

Проверяйте поведение

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

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

Опции анализа

развернуть все

Allow negative operand for left shifts (-allow-negative-operand-in-shift)Позвольте операции сдвига влево на отрицательном числе
Overflow mode for signed integer (-signed-integer-overflows)Задайте, переносится ли результат переполнения или усеченный
Overflow mode for unsigned integer (-unsigned-integer-overflows)Задайте, переносится ли результат переполнения или усеченный
Disable checks for non-initialization (-disable-initialization-checks)Отключите проверки на неинициализированные переменные и указатели
Check that global variables are initialized after warm reboot (-check-globals-init)Проверяйте, что глобальные переменные являются присвоенными значениями в спроектированном коде инициализации
Detect stack pointer dereference outside scope (-detect-pointer-escape)Найдите случаи, куда функция возвращает указатель на одну из его локальных переменных
Enable pointer arithmetic across fields (-allow-ptr-arith-on-struct)Позвольте арифметику на указателе на поле структуры так, чтобы это указало на другое поле
Allow incomplete or partial allocation of structures (-size-in-bytes)Позвольте указателю с буфером недостаточно памяти указывать на структуру
Permissive function pointer calls (-permissive-function-pointer)Позвольте несоответствие типов между указателями функции и функциями, на которые они указывают
Detect uncalled functions (-uncalled-function-checks)Обнаружьте функции, которые не вызваны прямо или косвенно от main или другая функция точки входа
Consider non finite floats (-allow-non-finite-floats)Включите аналитический режим, который включает бесконечности и NaNs
Infinities (-check-infinite)Задайте, как обработать операции с плавающей точкой тот результат в бесконечности
NaNs (-check-nan)Задайте, как обработать операции с плавающей точкой тот результат в NaN
Subnormal detection mode (-check-subnormal)Обнаружьте операции, которые приводят к субнормальным значениям с плавающей точкой

Темы

Задайте опции анализа Polyspace

Задайте опции анализа Polyspace® в пользовательском интерфейсе Polyspace, других IDE-s или скриптах.

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

Отключите подмножество проверок на этапе выполнения в Программе автоматического доказательства Кода

Обнаружьте переполнение в расчете Buffer Size

Обнаружьте переполнение ранее во время расчета buffer size вместо позже во время буферного использования.

Документация Polyspace Code Prover

Поддержка