Опции для управления созданием проекта Polyspace и последующим анализом. Вы в основном используете опции для устранения неполадок, например, чтобы выполнить только определенные части обновления и сузить проблему или предоставить дополнительные заголовочные файлы или задать макросы.
Общие опции
| Опция | Описание |
|---|
-verbose | Сохраните дополнительную информацию о различных фазах выполнения команды (подробный режим). Файл psar_project.log и другие вспомогательные файлы хранят эту дополнительную информацию. Если при выполнении команды возникает ошибка, сообщение об ошибке сохраняется в отдельном файле, независимо от того, включен ли подробный режим. Выполнение в подробном режиме хранит только различные фазы выполнения. Вы можете использовать эту информацию, чтобы увидеть, когда была введена ошибка. |
-options-file OPTION_FILE | Используйте файл параметров, чтобы дополнить или заменить опции командной строки. В файле опций задайте каждую опцию в отдельной линии. Начните линию с # для указания комментариев. Файл опций opts.txt может выглядеть следующим образом: # Store Polyspace results
-create-project polyspace
# ARXML Folder
-arxml-dir arxml
# SOURCE Folder
-sources-dir code Можно запустить polyspace-autosar как: polyspace-autosar -options-file opts.txt Если опция, непосредственно заданная в polyspace-autosar команда конфликтует с опцией в файле options, используется непосредственно заданная опция. Например, в этом примере папка proj используется для сохранения проекта Polyspace. polyspace-autosar -create-project proj -options-file opts.txt Обычно файл опций используется для хранения и повторного использования опций, общих для нескольких проектов. |
Опции для контроля обновления проекта
Если вы обновляете проект, по умолчанию результаты анализа обновляются для всех поведений AUTOSAR SWC в отношении любых изменений в файлах arxml или исходном коде C с момента последнего анализа. Эти опции позволяют управлять обновлением.
| Опция | Описание |
|---|
-автозар-поведение AUTOSAR_QUALIFIED_NAME | Проверяйте реализацию программных компонентов, внутреннее поведение которых определяется AUTOSAR_QUALIFIED_NAME. Анализ по умолчанию рассматривает все программные компоненты, существующие в спецификациях ARXML. Чтобы задать несколько программных компонентов, повторите опцию. Также можно выполнить одно из следующих действий:
Используйте шаблоны интерпретатора, аналогичные шаблонам, используемым с -select-arxml-files и -select-source-files. Для примеров смотрите Выбрать AUTOSAR XML (ARXML) и Файлы кода для анализа Polyspace. Используйте регулярные выражения, чтобы задать группу программных компонентов в том же пакете. Для образца:
Чтобы указать программный компонент, внутренне поведение которого имеет полное имя pkg.component.bhv, использовать: -autosar-behavior pkg.component.bhv Чтобы задать программные компоненты, внутреннее поведение которых имеет полные имена, начинающиеся с pkg.component, использовать: -autosar-behavior pkg.component\..* The \. представляет диафрагму имен пакетов . (точка) и .* представляет любое количество символов.
|
-do-not-update-autosar-prove-environment | Не считывайте спецификации ARXML. Используйте спецификации ARXML, сохраненные в предыдущем анализе. Используйте эту опцию во время обновления проекта, чтобы сравнить код с предыдущими спецификациями. Если вы не используете эту опцию, обновления проекта снова считывают все спецификации ARXML. |
-do-not-update-extract-code | Не считывайте исходный код C. Используйте исходный код, сохраненный из предыдущего анализа. Используйте эту опцию во время обновления проекта, чтобы сравнить предыдущий исходный код со спецификациями ARXML. Если вы не используете эту опцию, обновления проекта учитывают все изменения исходного кода со времени предыдущего анализа. |
-do-not-update-verification | Ознакомьтесь только со спецификациями ARXML и реализацией кода С, но не запускайте анализ Code Prover. Используйте эту опцию во время обновления проекта, чтобы исследовать ошибки, внесенные в спецификации ARXML или ошибки компиляции, введенные в исходный код. Можно сначала устранить эти проблемы, а затем запустить анализ Code Prover. |
Опции для управления синтаксическим анализом спецификаций ARXML
| Опция | Описание |
|---|
-autosar-datatype AUTOSAR_QUALIFIED_NAME | Определение импорта типов данных AUTOSAR, заданное AUTOSAR_QUALIFIED_NAME. Анализ по умолчанию импортирует только типы данных, заданные во внутреннем поведении проверяемых компонентов программного обеспечения. Чтобы задать несколько типов данных, повторите опцию. Также можно выполнить одно из следующих действий:
Используйте шаблоны интерпретатора, аналогичные шаблонам, используемым с -select-arxml-files и -select-source-files. Для примеров смотрите Выбрать AUTOSAR XML (ARXML) и Файлы кода для анализа Polyspace. Используйте регулярные выражения, чтобы задать все типы данных в одном пакете. Для образца:
Чтобы задать тип данных с полным именем pkg.datatypes.type, использовать: -autosar-datatype pkg.datatypes.type Чтобы задать типы данных с полными именами, начинающимися с pkg.datatypes, использовать: -autosar-datatype pkg.datatypes\..* The \. представляет диафрагму имен пакетов . (точка) и .* представляет любое количество символов.Чтобы принудительно импортировать все типы данных, используйте:
|
-Eautosar-xmlReaderSameUuidForDifferentElements
-Eno-autosar-xmlReaderSameUuidForDifferentElements
| Если несколько элементов спецификаций ARXML имеют одинаковый универсальный уникальный идентификатор (uuid), используйте эти опции, чтобы переключаться между предупреждением и ошибкой. Анализ по умолчанию останавливается с ошибкой, если произошла проблема. Для преобразования в предупреждение используйте -Eno-autosar-xmlReaderSameUuidForDifferentElements. Для конфликтующих UUID-ов анализ сохраняет последний элемент, считанный и продолжается с предупреждением. Последующие исполнения продолжают использовать режим предупреждения. Чтобы вернуться к ошибке, используйте -Eautosar-xmlReaderSameUuidForDifferentElements. |
-Eautosar-xmlReaderTooManyUuids
-Eno-autosar-xmlReaderTooManyUuids
| Если тот же элемент спецификаций ARXML имеет другие универсально-уникальные идентификаторы (uuid-s), используйте эти опции, чтобы переключаться между предупреждением и ошибкой. Анализ по умолчанию останавливается с ошибкой, если произошла проблема. Для преобразования в предупреждение используйте -Eno-autosar-xmlReaderTooManyUuids. Для конфликтующих UUID-ов анализ сохраняет последний элемент, считанный и продолжается с предупреждением. Последующие исполнения продолжают использовать режим предупреждения. Чтобы вернуться к ошибке, используйте -Eautosar-xmlReaderTooManyUuids. |
Опции для контроля чтения исходного кода C
| Опция | Описание |
|---|
-включите USER_RTE_TYPE_H | Задайте дополнительные типы данных и макросы, которые не являются частью спецификаций ARXML, но необходимы для анализа реализации кода. Добавьте тип данных и определения макросов к файлу USER_RTE_TYPE_H. Эти определения добавляются к файлу заголовка Rte_Type.h который используется в анализе. Файл, который вы предоставляете, не должен сам называться Rte_Type.h. Вы можете предоставить файлу тип данных и определения макросов только во время создания проекта. Для последующих обновлений можно изменить содержимое этого файла, но не предоставить новый файл. Кроме того, этот файл не должен находиться в той же папке, что и проект Polyspace, и результаты. Если вы дополнительно задаете макросы или не определяете их с помощью опций -D или -U, для определений, которые конфликтуют с таковыми в USER_RTE_TYPE_H, а -D или -U преобладают спецификации. |
-I INCLUDE_FOLDER | Укажите папки, содержащие заголовочные файлы. Анализ ищет #include-d файлы в этой папке. Папка должна быть подпапкой папки исходного кода. Повторите опцию для нескольких папок. Анализ ищет заголовочные файлы в этих папках в том порядке, в котором вы их задаете. Если необходимо указать папки, которые не находятся в папке исходного кода, используйте опцию: -extra-project-options "-I INCLUDE_FOLDER" |
-D DEFINE | Задайте макросы, которые анализ должен учитывать как определено. Например, если вы задаете: условный процессор препроцессора #ifdef _WIN32 успешно завершается, и выполняется соответствующая ветвь. |
-U UNDEFINE | Укажите макросы, которые анализ должен считать неопределенными. Например, если вы задаете: условный процессор препроцессора #ifndef _WIN32 успешно завершается, и выполняется соответствующая ветвь. |
Опции для кода системы управления проверок Prover
| Опция | Описание |
|---|
-extra-project-options POLYSPACE_OPTIONS | Задайте дополнительные опции для анализа Code Prover. Заданные опции применяются не к анализу ARXML или извлечению кода, а только к последующему анализу Code Prover. Используйте этот метод, чтобы задать опции анализа, которые вы используете с polyspace-code-prover команда. См. Опции анализа в Polyspace Code Prover. Для образца:
Обратите внимание, что эти опции polyspace-code-prover не нужно указывать:
-sources: polyspace-autosar извлекает необходимые исходные файлы.
-I: Вы задаете включить папки с -I опция polyspace-autosar.
Входы и опции упругости, такие как -data-range-specifications: Внешние ограничения данных в файлах ARXML автоматически извлекаются с помощью polyspace-autosar. Вы не можете задать ограничения явно. Опции многозадачности, такие как -entry-points: Вы не можете выполнить многозадачный анализ с polyspace-autosar. Чтобы обнаружить гонки данных, создайте отдельный проект для всего приложения и явным образом добавьте свои исходные папки. Укажите файлы ARXML, относящиеся к многозадачности, и запустите Bug Finder. Для получения дополнительной информации смотрите ARXML files selection (-autosar-multitasking). Опции верификации Code Prover, сопоставленные с main генерация: A main функция сгенерирована (в файле psar_prove_main.c) при создании проекта Polyspace из описания AUTOSAR. The main function вызовов функции, которые реализуют выполняемые сущности в компонентах программного обеспечения. Сгенерированный main необходим для анализа Code Prover. Вы не можете изменить свойства этого main функция.
|
-extra-options-file OPTIONS_FILE | Укажите дополнительные опции для анализа Code Prover в файле параметров. Заданные опции применяются не к анализу ARXML или извлечению кода, а только к последующему анализу Code Prover. Например, можно проследить команду build, чтобы собрать опции компилятора, определения макросов и пути, чтобы включить папки, и предоставить эту информацию в файл options для анализа реализации кода компонентов программного обеспечения AUTOSAR.
Проследите свою команду сборки (для образца, make) с polyspace-configure и сгенерируйте файл опций для последующего анализа Code Prover. Подавьте включение источников в файл опций с -no-sources опция. polyspace-configure -output-options-file options.txt -no-sources make Запустите Code Prover на коде AUTOSAR с polyspace-autosar. Укажите папку ARXML, исходные папки и другие опции. В сложение предоставьте ранее сгенерированный файл опций с -extra-options-file опция. polyspace-autosar ... -extra-options-file options.txt
Смотрите также Run Polyspace on AUTOSAR Code Using Build Command. |
-шоу-докажите AUTOSAR_QUALIFIED_NAME | После анализа откройте результаты для определенного программного компонента, внутреннее поведение которого определяется AUTOSAR_QUALIFIED_NAME. |