Опции, чтобы управлять созданием проекта 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 с опцией в файле опций, непосредственно заданной опцией, используется. Например, в этом примере, папка proj используется, чтобы сохранить проект Polyspace. polyspace-autosar -create-project proj -options-file opts.txt Вы обычно используете файл опций, чтобы сохранить и снова использовать опции, которые характерны для нескольких проектов. |
Опции, чтобы управлять обновлением проекта
Если вы обновляете проект, по умолчанию, результаты анализа обновляются для всех поведений AUTOSAR SWCs относительно любого изменения в arxml файлах или исходном коде C начиная с последнего анализа. Эти опции позволяют вам управлять обновлением.
| Опция | Описание |
|---|
-autosar-behavior AUTOSAR_QUALIFIED_NAME | Проверяйте реализацию компонентов программного обеспечения, внутренние поведения которых заданы AUTOSAR_QUALIFIED_NAME Чтобы задать несколько компонентов программного обеспечения, повторите опцию. Также используйте регулярные выражения, чтобы задать группу компонентов программного обеспечения под тем же пакетом. Например:
Чтобы задать компонент программного обеспечения, внутреннее поведение которого имеет полностью определенное имя pkg.component.bhv, используйте: -autosar-behavior pkg.component.bhv Чтобы задать компоненты программного обеспечения, внутренние поведения которых полностью определили имена, начинающиеся с pkg.component, используйте: -autosar-behavior pkg.component\..* . \ представляет разделитель имени пакета, . (точка) и .* представляет любое количество символов.
|
-do-not-update-autosar-prove-environment | Не читайте спецификации ARXML. Используйте спецификации ARXML, сохраненные от предыдущего анализа. Используйте эту опцию во время обновлений проекта, чтобы сравнить код с предыдущими спецификациями. Если вы не используете эту опцию, обновления проекта читают целые спецификации ARXML снова. |
-do-not-update-extract-code | Не читайте исходный код C. Используйте исходный код, сохраненный от предыдущего анализа. Используйте эту опцию во время обновлений проекта, чтобы сравнить предыдущий исходный код со спецификациями ARXML. Если вы не используете эту опцию, обновления проекта рассматривают все изменения в исходном коде начиная с предыдущего анализа. |
-do-not-update-verification | Считайте спецификации ARXML и реализацию кода С только, но не запускайте анализ Программы автоматического доказательства Кода. Используйте эту опцию во время обновлений проекта, чтобы исследовать ошибки, введенные в спецификациях ARXML или ошибках компиляции, введенных в исходном коде. Можно сначала устранить эти проблемы и затем запустить анализ Программы автоматического доказательства Кода. |
Опции, чтобы управлять парсингом спецификаций ARXML
| Опция | Описание |
|---|
-autosar-datatype AUTOSAR_QUALIFIED_NAME | Импортируйте определение типов данных AUTOSAR, заданных AUTOSAR_QUALIFIED_NAME. Анализ по умолчанию только импортирует типы данных, заданные во внутреннем поведении компонентов программного обеспечения, которые вы проверяете. Чтобы задать несколько типов данных, повторите опцию. Также используйте регулярные выражения, чтобы задать все типы данных под тем же пакетом. Например:
Чтобы задать тип данных, который имеет полностью определенное имя pkg.datatypes.type, используйте: -autosar-datatype pkg.datatypes.type Чтобы задать типы данных, которые полностью определили имена, начинающиеся с pkg.datatypes, используйте: -autosar-behavior pkg.datatypes\..* . \ представляет разделитель имени пакета, . (точка) и .* представляет любое количество символов.Чтобы обеспечить импорт всех типов данных, используйте:
|
-Eautosar-xmlReaderSameUuidForDifferentElements
-Eno-autosar-xmlReaderSameUuidForDifferentElements
| Если несколько элементов в спецификациях ARXML имеют тот же универсальный уникальный идентификатор (uuid), используйте эти опции, чтобы переключиться между предупреждением и ошибкой. Анализ по умолчанию останавливается с ошибкой, если проблема происходит. Чтобы преобразовать в предупреждение, используйте -Eno-autosar-xmlReaderSameUuidForDifferentElements. Для конфликта UUID-s анализ хранит последнее чтение элемента и продолжает предупреждение. Последующее выполнение продолжает использовать режим предупреждения. Чтобы вернуться назад к ошибке, используйте -Eautosar-xmlReaderSameUuidForDifferentElements. |
-Eautosar-xmlReaderTooManyUuids
-Eno-autosar-xmlReaderTooManyUuids
| Если тот же элемент в спецификациях ARXML имеет различные универсальные уникальные идентификаторы (uuid-s), используйте эти опции, чтобы переключиться между предупреждением и ошибкой. Анализ по умолчанию останавливается с ошибкой, если проблема происходит. Чтобы преобразовать в предупреждение, используйте -Eno-autosar-xmlReaderTooManyUuids. Для конфликта UUID-s анализ хранит последнее чтение элемента и продолжает предупреждение. Последующее выполнение продолжает использовать режим предупреждения. Чтобы вернуться назад к ошибке, используйте -Eautosar-xmlReaderTooManyUuids. |
Опции, чтобы управлять чтением исходного кода C
| Опция | Описание |
|---|
-include USER_RTE_TYPE_H | Задайте дополнительные типы данных и макросы, которые не являются частью ваших спецификаций ARXML, но необходимый для анализа реализации кода. Добавьте определения типов и макроопределения к файлу USER_RTE_TYPE_HRte_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 следует и соответствующее ответвление, выполняется. |
Опции к проверкам Программы автоматического доказательства кода системы управления
| Опция | Описание |
|---|
-extra-project-options POLYSPACE_OPTIONS | Задайте дополнительные опции для анализа Программы автоматического доказательства Кода. Опции, которые вы задаете, не применяются к парсингу ARXML или экстракции кода, но только к последующему анализу Программы автоматического доказательства Кода. Используйте этот метод, чтобы задать аналитические опции, которые вы используете с командой polyspace-code-prover. См. Аналитические Опции. Например:
Обратите внимание на то, что эти опции polyspace-code-prover не должны быть заданы:
-sources: polyspace-autosar извлекает необходимые исходные файлы.
i: Вы задаете, включают папки с опцией -I polyspace-autosar.
Входные параметры и Блокирующие опции, такие как -data-range-specifications: Внешние ограничения данных в ваших файлах ARXML извлечены автоматически с polyspace-autosar. Вы не можете задать ограничения явным образом. Многозадачные опции, такие как -entry-points: Вы не можете выполнить многозадачный анализ с polyspace-autosar. Чтобы обнаружить гонки данных, создайте отдельный проект для целого приложения и явным образом добавьте свои исходные папки. Задайте файлы ARXML, важные для многозадачности, и запустите Средство поиска Ошибки. Для получения дополнительной информации смотрите ARXML files selection (-autosar-multitasking). Опции Верификации Программы автоматического доказательства кода сопоставили с генерацией main: функция main сгенерирована (в файле psar_prove_main.c), когда вы создаете проект Polyspace из описания AUTOSAR. Функции вызовов функции main, которые реализуют выполнимые сущности в компонентах программного обеспечения. Сгенерированный main необходим для анализа Программы автоматического доказательства Кода. Вы не можете изменить свойства этой функции main. Опции Automatic Orange Tester: Вы не можете использовать Автоматический Оранжевый Тестер когда рабочий Polyspace на реализации кода компонентов программного обеспечения AUTOSAR.
|
-extra-options-file OPTIONS_FILE | Задайте дополнительные опции для анализа Программы автоматического доказательства Кода в файле опций. Опции, которые вы задаете, не применяются к парсингу ARXML или экстракции кода, но только к последующему анализу Программы автоматического доказательства Кода. Например, можно проследить команду сборки, чтобы собрать параметры компилятора, макроопределения и пути, чтобы включать папки и предоставить эту информацию в файле опций для анализа реализации кода компонентов программного обеспечения AUTOSAR.
Проследите свою команду сборки (например, make) с polyspace-configure и сгенерируйте файл опций для последующего анализа Программы автоматического доказательства Кода. Подавите включение источников в файле опций с опцией -no-sources. polyspace-configure -output-options-file options.txt -no-sources make Запустите Программу автоматического доказательства Кода на коде AUTOSAR с polyspace-autosar. Обеспечьте свою папку ARXML, исходные папки и другие опции. Кроме того, предоставьте ранее сгенерированному файлу опций опцию -extra-options-file. polyspace-autosar ... -extra-options-file options.txt
См. также Polyspace Выполнения на Коде AUTOSAR Используя Команду Сборки. |
-show-prove AUTOSAR_QUALIFIED_NAME | После анализа, открытых результатов для определенного компонента программного обеспечения, внутреннее поведение которого задано AUTOSAR_QUALIFIED_NAME. |
