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)Отключите проверки на неинициализированные переменные и указатели
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)Обнаружьте функции, которые не вызваны прямо или косвенно от основного или другой функции точки входа
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
Поддержка