Обнаружьте невостребованные функции (-uncalled-function-checks)

Обнаружьте функции, которые не вызваны прямо или косвенно от main или другой функции точки входа

Описание

Эта опция влияет на анализ Программы автоматического доказательства Кода только.

Обнаружьте функции, которые не вызваны прямо или косвенно от main или другой функции точки входа во время времени выполнения.

Установите опцию

Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция находится на узле Check Behavior.

Командная строка: Используйте опцию -uncalled-function-checks. Смотрите информацию о Командной строке.

Почему использование эта опция

Как правило, после верификации, панель Dashboard показывает функции, которые не вызваны во время верификации. Однако вы не видите их в своих результатах анализа или отчетах. Вы не можете прокомментировать их или выровнять по ширине их.

Если вы хотите видеть эти невостребованные функции в своих результатах анализа и отчетах, используйте эту опцию.

Настройки

Значение по умолчанию: none

none

Верификация не генерирует чеки для невостребованных функций.

never-called

Верификация генерирует чеки для функций, которые заданы, но не названы.

called-from-unreachable

Верификация генерирует чеки для функций, которые заданы и названы от недостижимой части кода.

all

Верификация генерирует чеки для функций, которые являются:

  • Заданный, но не названный

  • Заданный и названный от недостижимой части кода.

Информация о командной строке

Параметр: -uncalled-function-checks
Значение: none | never-called | called-from-unreachable | all
Значение по умолчанию: none
Пример (программа автоматического доказательства кода): polyspace-code-prover -sources file_name -uncalled-function-checks all
Пример (сервер программы автоматического доказательства кода): polyspace-code-prover-server -sources file_name -uncalled-function-checks all