Опции, чтобы управлять созданием проекта Polyspace и последующим анализом. Вы, в основном, используете опции в поиске и устранении неисправностей, например, чтобы только выполнить определенные части обновления и сузить проблему или обеспечить дополнительные заголовочные файлы или задать макросы.
Общие опции
| Опция | Описание |
|---|
-verbose | Сохраните дополнительную информацию о различных фазах выполнения команды (многословный режим). Файл psar_project.log и другие вспомогательные файлы хранят эту дополнительную информацию. Если ошибка происходит в выполнении команды, сообщение об ошибке хранится в отдельном файле, независимо от того, разрешаете ли вы многословный режим. Выполнение в многословном режиме только хранит различные фазы выполнения. Можно использовать эту информацию, чтобы видеть, когда ошибка была введена. |
- файл опций 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-поведение 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-тип-данных 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
| Опция | Описание |
|---|
- включайте USER_RTE_TYPE_H | Задайте дополнительные типы данных и макросы, которые не являются частью ваших спецификаций ARXML, но необходимый для анализа реализации кода. Добавьте определения типов и макроопределения к файлу USER_RTE_TYPE_HRte_Type.h это используется в анализе. Файл, который вы обеспечиваете, нельзя самостоятельно назвать Rte_Type.h. Можно предоставить файлу определения типов и макроопределения только во время создания проекта. Для последующих обновлений можно изменить содержимое этого файла, но не обеспечить новый файл. Кроме того, этот файл не должен быть в той же папке как проект Polyspace и результаты. Если вы дополнительно задаете макросы или не задаете их использующий опции -D или -U, для определений, которые конфликтуют с теми в USER_RTE_TYPE_H, -D или -U спецификации преобладают. |
- Я INCLUDE_FOLDER | Задайте папки, содержащие заголовочные файлы. Анализ ищет #include- d файлы в этой папке. Папка должна быть подпапкой вашей папки исходного кода. Повторите опцию для нескольких папок. Анализ ищет заголовочные файлы в этих папках в порядке, в котором вы задаете их. Если вы хотите задать папки, которые не находятся в папке исходного кода, используют опцию: -extra-project-options "-I INCLUDE_FOLDER" |
- D DEFINE | Задайте макросы, которые анализ должен рассмотреть, как задано. Например, если вы задаете: условное выражение препроцессора #ifdef _WIN32 успешно выполняется и соответствующая ветвь выполняется. |
- U UNDEFINE | Задайте макросы, которые анализ должен рассмотреть как неопределенные. Например, если вы задаете: условное выражение препроцессора #ifndef _WIN32 успешно выполняется и соответствующая ветвь выполняется. |
Опции к проверкам Программы автоматического доказательства кода системы управления
| Опция | Описание |
|---|
- дополнительные опции проекта 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.
|
- дополнительный файл опций 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 Используя Команду Сборки. |
- покажите - доказывают AUTOSAR_QUALIFIED_NAME | После анализа, открытых результатов для определенного компонента программного обеспечения, внутреннее поведение которого задано AUTOSAR_QUALIFIED_NAME. |
