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 Code Prover Server
Поддержка