Exponenta Banner
exponenta event banner

Используемые библиотеки (-library)

Укажите библиотеки, используемые в программе

Описание

Укажите библиотеки, используемые в программе.

Анализ использует смарт-заглушки для функций из этих библиотек вместо общих заглушек и не пытается проверить реализации функций. Использование этой опции обеспечивает более быстрый анализ без потери точности и инициирует специфичные для библиотеки проверки вызовов функций.

Задать опцию

Пользовательский интерфейс (только для настольных ПК): в конфигурации проекта параметр находится в узле Inputs & Stubbing.

файл командной строки и параметров: Использовать параметр -library. См. раздел Сведения о командной строке.

Зачем использовать этот параметр

Для более быстрого анализа с учетом библиотеки используйте этот параметр. Если эта опция не используется, анализ либо пытается проверить реализацию библиотеки, либо, если реализация недоступна, использует общие заглушки для функций библиотеки. Проверка тел функций может значительно увеличить время анализа при использовании общих заглушек может привести к потере точности.

Опция также инициирует специфичные для библиотеки проверки аргументов функции. Например, при выборе значения опции autosarАнализ Bug Finder или Code Prover проверяет аргументы функций из API AUTOSAR RTE на соответствие стандарту AUTOSAR.

Настройки

По умолчанию: none

none

Анализ использует смарт-заглушки только для функций из стандартной библиотеки C или C++ (если их реализации не удается найти).

autosar

Помимо остановки функций стандартной библиотеки C или C++ с отсутствующими реализациями, анализ использует смарт-заглушки для функций AUTOSAR RTE API (даже если их реализации доступны).

Опция также запускает специфичные для AUTOSAR проверки аргументов функции. Для получения дополнительной информации см. соответствующие шашки:

  • Поиск ошибок: Non-compliance with AUTOSAR specification

    Помимо настройки параметра, необходимо также явно включить вышеупомянутую проверку (или включить все проверки).

  • Проверка кода: Non-compliance with AUTOSAR specification(Доказательство кода Polyspace)

    Для включения средства проверки достаточно установить этот параметр.

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

Параметр: -library
По умолчанию нет
Значение: autosar
Пример (поиск ошибок): polyspace-bug-finder -sources file_name -library autosar -checkers autosar_lib_non_compliance
Пример (проверка кода): polyspace-code-prover -sources file_name -library autosar
Пример (сервер поиска ошибок): polyspace-bug-finder-server -sources file_name -library autosar -checkers autosar_lib_non_compliance
Пример (сервер проверки кода): polyspace-code-prover-server -sources file_name -library autosar

См. также

Темы

Представлен в R2021a

Документация для поиска ошибок Polyspace

Поддержка