Опции, чтобы управлять созданием проекта 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 Чтобы задать несколько компонентов программного обеспечения, повторите опцию. В качестве альтернативы можно выполнить одно из следующих действий:
Используйте шаблоны интерпретатора, похожие на шаблоны, используемые с -select-arxml-files и -select-source-files. Для примеров смотрите, Выбирают AUTOSAR XML (ARXML) и Code Files for Polyspace Analysis. Используйте регулярные выражения, чтобы задать группу компонентов программного обеспечения под тем же пакетом. Например:
Задавать компонент программного обеспечения, внутреннее поведение которого имеет полностью определенное имя 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. Анализ по умолчанию только импортирует типы данных, заданные во внутреннем поведении компонентов программного обеспечения, которые вы проверяете. Чтобы задать несколько типов данных, повторите опцию. В качестве альтернативы можно выполнить одно из следующих действий:
Используйте шаблоны интерпретатора, похожие на шаблоны, используемые с -select-arxml-files и -select-source-files. Для примеров смотрите, Выбирают AUTOSAR XML (ARXML) и Code Files for Polyspace Analysis. Используйте регулярные выражения, чтобы задать все типы данных под тем же пакетом. Например:
Задавать тип данных, который имеет полностью определенное имя pkg.datatypes.typeИспользование: -autosar-datatype pkg.datatypes.type Задавать типы данных, которые полностью определили имена, начинающиеся с pkg.datatypesИспользование: -autosar-datatype 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-server команда. См. Аналитические Опции. Например:
В десктопных решениях вы можете хотеть, чтобы верификация была выполнена на удаленном кластере и результатах, загруженных на Метрики Polyspace. Введите эту расширенную настройку: -extra-project-options "-add-to-results-repository -batch -scheduler localhost" localhost указывает, что тот же компьютер служит сервером и клиентом. Замените его на имя вашего сервера. См. также Run Bug Finder or Code Prover analysis on a remote cluster (-batch) (Polyspace Code Prover) и Upload results to Polyspace Metrics (-add-to-results-repository) (Polyspace Code Prover).Вы можете хотеть задать компилятор и целевую архитектуру. По умолчанию компиляция проектов, созданных из технических требований AUTOSAR, использует gnu4.7 компилятор и i386 архитектуру. Чтобы задать visual11.0 компилятор с x86_64 архитектурой, введите эту опцию: -extra-project-options "-compiler visual11.0 -target x86_64" Compiler (-compiler) и Target processor type (-target).
Обратите внимание на то, что эти опции 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) (Polyspace Bug Finder). Опции Верификации Программы автоматического доказательства кода сопоставлены с main генерация: main функция сгенерирована (в файле psar_prove_main.c) когда вы создаете проект Polyspace из описания AUTOSAR. main функции вызовов функции, которые реализуют выполнимые сущности в компонентах программного обеспечения. Сгенерированный main необходим для анализа Программы автоматического доказательства Кода. Вы не можете изменить свойства этого main функция.
|
- дополнительный файл опций 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 Используя Команду Сборки (Polyspace Code Prover). |
- покажите - доказывают AUTOSAR_QUALIFIED_NAME | После анализа, открытых результатов для определенного компонента программного обеспечения, внутреннее поведение которого задано AUTOSAR_QUALIFIED_NAME. |
