Выполните один или несколько из этих шагов, пока вы не определите фиксацию для проверки Function not called. Существует несколько способов зафиксировать эту проверку. Для описания проверки и примеров кода, смотрите Function not called
.
Если вы решаете, что проверка представляет защитный код или функцию, которая является частью библиотеки, добавьте комментарий и выравнивание в вашем результате или коде, объясняющем, почему вы не изменили свой код. Смотрите Результаты Polyspace Адреса Через Исправления ошибок или Комментарии.
Эта проверка не включена по умолчанию. Чтобы включить эту проверку, необходимо задать соответствующую аналитическую опцию. Для получения дополнительной информации смотрите Detect uncalled functions (-uncalled-function-checks)
.
На панели Results List выберите проверку. На панели Source тело функции подсвечено в сером.
Ищите имя функции и смотрите, можно ли найти вызов функции в коде.
На панели Search введите имя функции. Из выпадающего списка около поля поиска выберите Source.
Возможная фиксация: Если вы не находите вызов функции, определяете, почему функциональное определение существует в вашем коде.
Если вы находите вызов функции, смотрите, происходит ли она в теле другой невостребованной функции.
Возможная фиксация: Займитесь расследованиями, почему последняя функция не вызвана.
Смотрите, вызываете ли вы функцию косвенно, например, через указатели функции.
Если косвенность слишком глубока, Polyspace® иногда не может решать, что вызвана определенная функция.
Возможная фиксация: Если Polyspace не может решить, что вы вызываете функцию косвенно, необходимо проверить функцию отдельно. Вы не должны писать новую функцию main
для этой другой верификации. Polyspace может сгенерировать функцию main
, если вы не обеспечиваете один в вашем источнике. Можно изменить опции генерации main
в случае необходимости. Для получения дополнительной информации об опциях смотрите Верификацию Программы автоматического доказательства Кода.
Ищите следующие частые причины проверки Function not called.
Определите, намеревались ли вы вызвать функцию, но использовали другую функцию вместо этого.
Определите, намеревались ли вы заменить некоторый код на вызов функции. Вы записали функциональное определение, но забыли заменять оригинальный код на вызов функции.
Если эта ситуация произойдет, у вас, вероятно, будет дублирующий код.
Смотрите, намереваетесь ли вы вызвать функцию из уже незаписанного кода. Если так, сохраните функциональное определение.
Для кода, предназначенного для многозадачности, смотрите, задали ли вы все свои функции точки входа.
Чтобы видеть опции, используемые для результата, выберите ссылку View configuration for results на панели Dashboard.
Для получения дополнительной информации смотрите Tasks (-entry-points)
.
Для кода, предназначенного для многозадачности, смотрите, содержит ли ваша функция main
бесконечный цикл. Polyspace Code Prover™ требует, чтобы ваша функция main
завершила выполнение, прежде чем другие точки входа начнутся.
Для получения дополнительной информации смотрите Анализ Многозадачности Polyspace Конфигурирования Вручную.