exponenta event banner

polyspace-autosar

(DOS/UNIX) Запуск Polyspace Code Prover для реализации кода программных компонентов AUTOSAR

Описание

пример

polyspace-autosar -create-project projectFolder -arxml-dir arxmlFolder -sources-dir codeFolder [-sources-dir codeFolder] [OPTIONS] проверяет реализацию кода программных компонентов AUTOSAR на наличие ошибок времени выполнения и нарушение ограничений данных в соответствующих спецификациях AUTOSAR XML. Анализ анализирует спецификации AUTOSAR XML (.arxml файлы) в arxmlFolder, модулирует реализацию кода (.c файлы) в codeFolder на основе спецификаций и запускает Code Prover на каждом модуле для проверок. Результаты Code Prover хранятся в projectFolder. После анализа можно открыть проект psar_project.psprj от projectFolder в Polyspace® пользовательский интерфейс. Можно просмотреть результаты для каждого программного компонента по отдельности или загрузить их в Polyspace Metrics для обзора.

Можно использовать дополнительные опции для устранения неполадок, например, чтобы выполнить только определенные части обновления и отследить проблему или предоставить дополнительные заголовочные файлы или задать макросы.

polyspace-autosar -create-project projectFolder -select-arxml-files arxmlFiles [-select-arxml-files arxmlFiles] -select-source-files codeFiles [-select-source-files codeFiles] [OPTIONS] создает проект Polyspace из спецификаций AUTOSAR, как и в предыдущем синтаксисе, но позволяет исключить определенные файлы или папки из анализа с помощью шаблонов интерпретатора или регулярных выражений.

пример

polyspace-autosar -update-project prevProjectFile [OPTIONS] обновляет результаты анализа Code Prover на основе изменений в файлах ARXML или исходном коде C с момента последнего анализа. Обновление использует html- файл prevProjectFile из предыдущего анализа и только повторно анализирует реализацию кода программных компонентов, которые изменились после этого анализа.

Для устранения неполадок можно использовать дополнительные опции.

пример

polyspace-autosar -update-and-clean-project prevProjectFile [OPTIONS] обновляет результаты анализа Code Prover на основе изменений в файлах ARXML или исходном коде C с момента последнего анализа. Обновление только повторно анализирует реализацию кода программных компонентов, которая изменилась со времени предыдущего анализа. Чистое обновление также удаляет информацию о программных компонентах, которые устарели. Например, если вы используете дополнительную опцию, чтобы форсировать обновление для определенных программных компонентов, и другие SWC-ы также изменились, чистое обновление удаляет эти другие SWC-ы из проекта Polyspace.

Для устранения неполадок можно использовать дополнительные опции.

polyspace-autosar -help показывает все опции, доступные для polyspace-autosar.

Примеры

свернуть все

Предположим, ваши файлы ARXML находятся в папке arxml и ваши исходные файлы C в папке code в текущей папке.

Запустите Code Prover для всех программных компонентов, определенных в ваших файлах ARXML. Сохраните результаты в папке polyspace в текущей папке.

polyspace-autosar -create-project polyspace -arxml-dir arxml -sources-dir code

Анализ создает проект Polyspace с несколькими модулями. Каждый модуль собирает реализацию кода С программного компонента. Анализ запускает Code Prover на каждом модуле и проверяет код на ошибки времени выполнения или несоответствие спецификациям ARXML.

После анализа можно открыть результаты несколькими способами. Смотрите Обзор результатов Polyspace на AUTOSAR Code.

Обновление файла кода или ARXML. Например, в Linux®, можно touch файл для указания обновления. Проверьте, влияют ли обновления на результаты анализа Code Prover. Для обновленного анализа предоставьте файл проекта psar_project.html созданный на предыдущем шаге.

polyspace-autosar -update-project polyspace\psar_project.xhtml

Если вы обновляете файл ARXML, весь анализ повторяется. Если вы обновляете свой исходный код, анализ повторяется только для компонентов программного обеспечения, реализация кода которых была обновлена.

Вместо запуска Code Prover для всех компонентов программного обеспечения проверьте только определенные компоненты программного обеспечения.

Например, предположим, что программный компонент имеет полный путь pkg.component.bhv. Запускать Code Prover можно только на этом программном компоненте.

polyspace-autosar -create-project polyspace -arxml-dir arxml -sources-dir code -autosar-behavior pkg.component.bhv

Можно запустить Code Prover для всех компонентов программного обеспечения, но позже выберите обновить анализ только для определенных компонентов программного обеспечения.

polyspace-autosar -update-project polyspace\psar_project.xhtml -autosar-behavior pkg.component.bhv

Если вы не повторно анализируете обновленный программный компонент, анализ показывает, что программный компонент может быть устаревшим.

Можно также обновить анализ для определенных компонентов программного обеспечения и удалить все трассировки других компонентов программного обеспечения.

polyspace-autosar -update-and-clean-project polyspace\psar_project.xhtml -autosar-behavior pkg.component.bhv

В пользовательском интерфейсе Polyspace можно увидеть результаты для отдельных компонентов программного обеспечения. Чтобы увидеть обзор результатов Code Prover для всех проанализированных компонентов программного обеспечения, загрузите результаты в Polyspace Metrics.

При выполнении верификации на сервере можно указать перед верификацией, что все результаты должны быть загружены в метрики Polyspace. Укажите удаленную верификацию и загрузку результатов с помощью следующих дополнительных опций:

Можно задать дополнительные опции с флагом -extra-project-options.

Для образца:

polyspace-autosar -create-project polyspace -arxml-dir arxml -sources-dir code -extra-project-options "-add-to-results-repository -batch -scheduler localhost -prog polyspace_project"
Вот localhost указывает, что тот же компьютер служит сервером и клиентом. Замените его на имя сервера. Аргумент -prog может быть таким же, как у -create-project. Вы используете опции -prog и -verif-version чтобы задать имя проекта и номер версии в том виде, в котором она отображается в Polyspace Metrics.

Также можно запустить Code Prover и загрузить каждый результат, используя polyspace-results-repository команда.

Входные параметры

свернуть все

Имя папки, заданное как строка (в двойных кавычках). Если папка существует, она должна быть пустой.

После анализа папка содержит два файла проекта psar_project.psprj и psar_project.html.

  • Чтобы увидеть результаты, откройте файл psar_project.psprj в пользовательском интерфейсе Polyspace или файле psar_project.html в веб-браузере.

  • Для последующих обновлений в командной строке используйте файл psar_project.html.

Смотрите также Обзор результатов Polyspace на коде AUTOSAR.

Пример: "C:\Polyspace_Projects\proj_swc1"

Имя папки, заданное как строка (в двойных кавычках). Можно опустить двойные кавычки, если пути к папкам не содержат пространств.

UNC- путей не поддерживаются для имени папки.

Пример: "C:\arxml_swc1"

Имя папки, заданное как строка (в двойных кавычках). Можно опустить двойные кавычки, если пути к папкам не содержат пространств.

Чтобы задать несколько корневых папок, содержащих источники, повторите -sources-dir опция. Если вы задаете несколько корневых папок, они не должны перекрываться. Например, одна корневая папка не может быть подпапкой другой.

UNC- путей не поддерживаются для имени папки.

Пример: "C:\code_swc1"

Корневая папка, содержащая файлы ARXML, с последующим включением файлов и папок и исключениями, заданными как строка. Чтобы создать эту строку:

  1. Используйте find Linux команда для поиска включаемых и исключаемых файлов и папок.

  2. Скопируйте find опции и заключайте их в двойные кавычки.

Для примеров смотрите Выбрать AUTOSAR XML (ARXML) и Файлы кода для анализа Polyspace.

Корневая папка, содержащая код (.c и .h) файлы, за которыми следуют включения и исключения файлов и папок, заданные как строка. Чтобы создать эту строку:

  1. Используйте find Linux команда для поиска включаемых и исключаемых файлов и папок.

  2. Скопируйте find опции и заключайте их в двойные кавычки.

Для примеров смотрите Выбрать AUTOSAR XML (ARXML) и Файлы кода для анализа Polyspace.

Путь к ранее созданному файлу проекта psar_project.html, заданный как строка (в двойных кавычках). Можно опустить двойные кавычки, если пути к папкам не содержат пространств.

Пример: "C:\Polyspace_Projects\proj1\psar_project.html"

Опции для управления созданием проекта 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 \. представляет диафрагму имен пакетов . (точка) и .* представляет любое количество символов.

    • Чтобы принудительно импортировать все типы данных, используйте:

      -autosar-datatype .*\..*

-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

Задайте макросы, которые анализ должен учитывать как определено.

Например, если вы задаете:

-D _WIN32
условный процессор препроцессора #ifdef _WIN32 успешно завершается, и выполняется соответствующая ветвь.

-U UNDEFINE

Укажите макросы, которые анализ должен считать неопределенными.

Например, если вы задаете:

-U _WIN32
условный процессор препроцессора #ifndef _WIN32 успешно завершается, и выполняется соответствующая ветвь.

Опции для кода системы управления проверок Prover

ОпцияОписание
-extra-project-options POLYSPACE_OPTIONS

Задайте дополнительные опции для анализа Code Prover. Заданные опции применяются не к анализу ARXML или извлечению кода, а только к последующему анализу Code Prover.

Используйте этот метод, чтобы задать опции анализа, которые вы используете с polyspace-code-prover команда. См. Опции анализа в Polyspace Code Prover.

Для образца:

  • В продуктах рабочего стола может потребоваться выполнить верификацию на удаленном кластере и загрузить результаты в Polyspace Metrics. Введите эту расширенную опцию:

    -extra-project-options "-add-to-results-repository -batch -scheduler localhost"
    Вот localhost указывает, что тот же компьютер служит сервером и клиентом. Замените его на имя сервера. См. также Run Bug Finder or Code Prover analysis on a remote cluster (-batch) и Upload results to Polyspace Metrics (-add-to-results-repository).

  • Можно хотеть задать компилятор и целевую архитектуру. По умолчанию при компиляции проектов, созданных из спецификаций 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, относящиеся к многозадачности, и запустите 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.

  1. Проследите свою команду сборки (для образца, make) с polyspace-configure и сгенерируйте файл опций для последующего анализа Code Prover. Подавьте включение источников в файл опций с -no-sources опция.

    polyspace-configure -output-options-file options.txt -no-sources make
  2. Запустите 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.

Введенный в R2018a