Exponenta Banner
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]
polyspace-autosar -create-project projectFolder -select-arxml-files arxmlFiles [-select-arxml-files arxmlFiles] -select-source-files codeFiles [-select-source-files codeFiles] [OPTIONS]
polyspace-autosar -update-project prevProjectFile [OPTIONS]
polyspace-autosar -update-and-clean-project prevProjectFile [OPTIONS]
polyspace-autosar -help

Описание

пример

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

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

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] обновляет результаты анализа Программы автоматического доказательства Кода на основе изменений в файлах ARXML или исходном коде C начиная с последнего анализа. Обновление использует файл HTML prevProjectFile от предыдущего анализа и только повторно анализирует реализацию кода компонентов программного обеспечения, которые изменились начиная с того анализа.

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

пример

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

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

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

Примеры

свернуть все

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

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

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

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

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

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

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

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

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

Например, предположите, что компонент программного обеспечения имеет полностью определенный путь pkg.component.bhv. Можно запустить Программу автоматического доказательства Кода только на этом компоненте программного обеспечения.

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

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

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 вы видите результаты для отдельных компонентов программного обеспечения. Чтобы видеть обзор результатов Программы автоматического доказательства Кода для всех анализируемых компонентов программного обеспечения, загрузите результаты на Метрики Polyspace.

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

В качестве альтернативы можно запустить Программу автоматического доказательства Кода и загрузить каждый результат с помощью 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) и Code Files for Polyspace Analysis.

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

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

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

Для примеров смотрите, Выбирают AUTOSAR XML (ARXML) и Code Files for Polyspace Analysis.

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

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

Опции, чтобы управлять созданием проекта 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. Анализ по умолчанию считает все компоненты программного обеспечения существующими в технических требованиях ARXML.

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

  • Используйте шаблоны интерпретатора, похожие на шаблоны, используемые с -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\..*
      \. представляет диафрагму имени пакета . (точка) и .* представляет любое количество символов.

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

      -autosar-datatype .*\..*

-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_H. Эти определения добавлены к заголовочному файлу Rte_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

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

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

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

- U UNDEFINE

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

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

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

Опции к проверкам Программы автоматического доказательства кода системы управления

ОпцияОписание
- дополнительные опции проекта POLYSPACE_OPTIONS

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

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

Например:

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

    -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).

  • Опции Верификации Программы автоматического доказательства кода сопоставлены с main генерация: main функция сгенерирована (в файле psar_prove_main.c) когда вы создаете проект Polyspace из описания AUTOSAR. main функции вызовов функции, которые реализуют выполнимые сущности в компонентах программного обеспечения. Сгенерированный main необходим для анализа Программы автоматического доказательства Кода. Вы не можете изменить свойства этого main функция.

- дополнительный файл опций OPTIONS_FILE

Задайте дополнительные опции для анализа Программы автоматического доказательства Кода в файле опций. Опции, которые вы задаете, не применяются к парсингу ARXML или экстракции кода, но только к последующему анализу Программы автоматического доказательства Кода.

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

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

    polyspace-configure -output-options-file options.txt -no-sources make

  2. Запустите Программу автоматического доказательства Кода на коде AUTOSAR с polyspace-autosar. Обеспечьте свою папку ARXML, исходные папки и другие опции. Кроме того, предоставьте ранее сгенерированному файлу опций -extra-options-file опция.

    polyspace-autosar ... -extra-options-file options.txt

См. также Polyspace Запуска на Коде AUTOSAR Используя Команду Сборки.

- покажите - доказывают AUTOSAR_QUALIFIED_NAME

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

Смотрите также

| | |

Темы

Введенный в R2018a

Документация Polyspace Code Prover

Поддержка