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 или скриптах.

Изменение или отключение проверок во время выполнения Code Prover

Отключите подмножество проверок во время выполнения в Code Prover

Обнаружение переполнений при расчете Buffer size

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

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

Поддержка