Exponenta Banner

polyspaceAutosar

Запустите Polyspace Code Prover на реализации кода компонентов программного обеспечения AUTOSAR с помощью скриптов MATLAB

свернуть все на странице

Синтаксис

[status, msg] = polyspaceAutosar('-create-project',projectFolder,'-arxml-dir',arxmlFolder,'-sources-dir',codeFolder,options)
[status, msg] = polyspaceAutosar('-update-project',prevProjectFile,options)
[status, msg] = polyspaceAutosar('-update-and-clean-project',prevProjectFile,options)
[status, msg, out] = polyspaceAutosar(___)

Описание

пример

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

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

[status, msg] = polyspaceAutosar('-update-project',prevProjectFile,options) обновляет результаты анализа Программы автоматического доказательства Кода на основе изменений в файлах ARXML или исходном коде C начиная с последнего анализа. Обновление использует файл XHTML prevProjectFile от предыдущего анализа и повторно анализирует только реализацию кода компонентов программного обеспечения, которые изменились начиная с того анализа.

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

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

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

[status, msg, out] = polyspaceAutosar(___) запускает анализ Программы автоматического доказательства Кода с помощью тех же опций как прежде. Вывод, вместо того, чтобы появиться в Командном окне MATLAB®, перенаправляется к вектору символов out.

Примечание

Прежде чем вы запустите Polyspace из MATLAB, необходимо соединить Polyspace и установки MATLAB. Смотрите Интегрируют Polyspace с MATLAB и Simulink.

Примеры

свернуть все

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

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

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

exampleDir = fullfile(polyspaceroot,'help',...
    'toolbox','codeprover','examples','polyspace_autosar');
arxmlDir = fullfile(exampleDir, 'arxml');
sourceDir = fullfile(exampleDir, 'code');

tempDir = tempdir;
projectDir = fullfile(tempDir, 'polyspace-project');
prevProjectFile = fullfile(projectDir, 'psar_project.xhtml');

% Update project file if it already exists, else create new project
projectDirAlreadyExists = isfolder(projectDir);

if projectDirAlreadyExists
    [status, msg] = polyspaceAutosar('-update-project', ...
        prevProjectFile);
else
    [status, msg] = polyspaceAutosar('-create-project', projectDir, ...
    '-arxml-dir', arxmlDir, ...
    '-sources-dir', sourceDir);
end

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

свернуть все

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

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

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

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

См. также Результаты Polyspace Анализа на Коде AUTOSAR.

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

Имя папки, заданное как вектор символов.

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

Имя папки, заданное как вектор символов.

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

Путь к ранее созданному файлу проекта psar_project.xhtml, заданный как вектор символов.

Пример: 'C:\Polyspace_Projects\proj1\psar_project.xhtml'

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

Задайте каждую опцию как вектор символов, сопровождаемый значением опции как отдельный вектор символов. Например, можно задать файл опций opts.txt при помощи синтаксиса polyspaceAutosar(...,'-options-file','opts.txt').

Общие опции

ОпцияЗначениеОписание
'-verbose' 

Сохраните дополнительную информацию о различных фазах выполнения команды (многословный режим). Файл psar_project.log и другие вспомогательные файлы хранит эту дополнительную информацию.

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

'-options-file'Имя файла опций, например, 'opts.txt'.

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

Файл опций opts.txt может выглядеть так:

# Store Polyspace results
-create-project polyspace
# ARXML Folder
-arxml-dir arxml
# SOURCE Folder
-sources-dir code

Если опция, которая непосредственно задана с конфликтами функции polyspaceAutosar с опцией в файле опций, непосредственно заданной опцией, используется.

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

Опции, чтобы управлять обновлением проекта

Если вы обновляете проект, по умолчанию, результаты анализа обновляются для всех поведений AUTOSAR SWC относительно любого изменения в файлах ARXML или исходном коде C начиная с последнего анализа. Управляйте обновлением при помощи этих опций.

ОпцияЗначениеОписание
'-autosar-behavior'Полное полностью определенное имя поведения SWC, например, 'pkg.component.bhv'.

Проверяйте реализацию компонентов программного обеспечения, внутренние поведения которых заданы. Анализ по умолчанию считает все компоненты программного обеспечения существующими в спецификациях ARXML.

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

Например:

  • Чтобы задать компонент программного обеспечения, внутреннее поведение которого имеет полностью определенное имя pkg.component.bhv, используйте:

    polyspaceAutosar(...,
'-autosar-behavior',...
'pkg.component.bhv')

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

    polyspaceAutosar(...,
'-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'Полное полностью определенное имя типа данных, например, 'pkg.datatypes.type'

Импортируйте определение заданных типов данных AUTOSAR. Анализ по умолчанию импортирует только типы данных, заданные во внутреннем поведении компонентов программного обеспечения, которые вы проверяете.

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

Например:

  • Чтобы задать тип данных, который имеет полностью определенное имя pkg.datatypes.type, используйте:

    polyspaceAutosar(...,
'-autosar-datatype',...
'pkg.datatypes.type')

  • Чтобы задать типы данных, которые полностью определили имена, начинающиеся с pkg.datatypes, используйте:

    polyspaceAutosar(...,
'-autosar-datatype',...
'pkg.datatypes\..*')
    . \ представляет разделитель имени пакета, . (точка) и .* представляет любое количество символов.

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

    polyspaceAutosar(...,
'-autosar-datatype',...
'.*\..*')

'-Eautosar-xmlReaderSameUuidForDifferentElements'

'-Eno-autosar-xmlReaderSameUuidForDifferentElements'

 

Если несколько элементов в спецификациях ARXML имеют тот же универсальный уникальный идентификатор (UUID), используйте эти опции, чтобы переключиться между предупреждением и ошибкой.

Анализ по умолчанию останавливается с ошибкой, если эта проблема происходит. Чтобы преобразовать в предупреждение, используйте '-Eno-autosar-xmlReaderSameUuidForDifferentElements'. Для конфликта UUIDs анализ хранит последнее чтение элемента и продолжает предупреждение.

Последующее выполнение продолжает использовать режим предупреждения. Чтобы вернуться назад к ошибке, используйте '-Eautosar-xmlReaderSameUuidForDifferentElements'.

'-Eautosar-xmlReaderTooManyUuids'

'-Eno-autosar-xmlReaderTooManyUuids'

 

Если тот же элемент в спецификациях ARXML имеет различные универсальные уникальные идентификаторы (UUID), используйте эти опции, чтобы переключиться между предупреждением и ошибкой.

Анализ по умолчанию останавливается с ошибкой, если эта проблема происходит. Чтобы преобразовать в предупреждение, используйте '-Eno-autosar-xmlReaderTooManyUuids'. Для конфликта UUIDs анализ хранит последнее чтение элемента и продолжает предупреждение.

Последующее выполнение продолжает использовать режим предупреждения. Чтобы вернуться назад к ошибке, используйте '-Eautosar-xmlReaderTooManyUuids'.

Опции, чтобы управлять чтением исходного кода C

ОпцияЗначениеОписание
'-include'Файл с определениями типов и макроопределениями.

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

Добавьте определения типов и макроопределения к файлу. Эти определения добавлены к заголовочному файлу Rte_Type.h, который используется в анализе. Файл, который вы обеспечиваете, нельзя самостоятельно назвать Rte_Type.h.

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

Если вы дополнительно задаете макросы или не задаете их использующий опции '-D' или '-U' для определений, которые конфликтуют с теми в USER_RTE_TYPE_H, -D или спецификации -U преобладают.

'-I'Папка, содержащая заголовочные файлы.

Задайте папки, содержащие заголовочные файлы. Анализ ищет #include-d файлы в этой папке. Папка должна быть подпапкой вашей папки исходного кода.

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

Если вы хотите задать папки, которые не находятся в папке исходного кода, используют опцию:

polyspaceAutosar(...,
 '-extra-project-options','-I INCLUDE_FOLDER')

'-D'Имя макроса, например, '_WIN32.

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

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

polyspaceAutosar(...,
 '-D','_WIN32')
условное выражение препроцессора, за которым #ifdef _WIN32 следует и соответствующее ответвление, выполняется.

'-U'Имя макроса, например, '_WIN32.

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

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

polyspaceAutosar(...,
 '-U','_WIN32')
условное выражение препроцессора, за которым #ifndef _WIN32 следует и соответствующее ответвление, выполняется.

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

ОпцияЗначениеОписание
'-extra-project-options'Разделенный пробелом список опций.

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

Используйте этот метод, чтобы задать аналитические опции, которые используются в non-AUTOSAR анализе Программы автоматического доказательства Кода. См. Аналитические Опции.

Например, вы можете хотеть задать компилятор и целевую архитектуру. По умолчанию компиляция проектов, созданных из спецификаций AUTOSAR, использует gnu4.7 компилятор и i386 архитектуру.

Чтобы задать visual11.0 компилятор с x86_64 архитектурой, введите эту опцию:

polyspaceAutosar(...,
 '-extra-project-options','-compiler visual11.0 -target x86_64')
См. также Compiler (-compiler) и Target processor type (-target).

'-extra-options-file'Файл с опциями Polyspace.

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

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

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

    polyspaceConfigure -output-options-file options.txt -no-sources make

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

    polyspaceAutosar(...,
 '-extra-options-file','options.txt')

'-show-prove'Полное полностью определенное имя поведения SWC, например, 'pkg.component.bhv'.

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

Выходные аргументы

свернуть все

Булев флаг, указывающий, выполнение ли анализ до завершения. Если анализ завершается, возвращаемое значение 0, в противном случае это - ненулевое значение.

Если вы видите ненулевое значение, проверяйте второй выходной аргумент polyspaceAutosar для сообщений об ошибке.

Можно также искать сообщения об ошибке в файле psar_project.xhtml в папке проекта. Можно использовать этот файл XHTML, чтобы определить, какие компоненты программного обеспечения анализировались.

Смотрите анализ Polyspace поиска и устранения неисправностей кода AUTOSAR.

Аналитический журнал, заданный как структура с этими полями:

Тип сообщения, возвращенного как один из трех векторов символов:

  • информация: информация, такая как текущий этап анализа.

  • Предупреждение: Предупреждения, которые не останавливают анализ, но могут вызвать ошибки позже.

  • ошибка: Ошибки, которые могут остановить целый анализ или анализ определенных компонентов программного обеспечения.

Чтобы проверить ошибки, используйте эту информацию о типе. Например, чтобы проверить ошибки в структуре в msg, используйте этот код:

% Convert to table for logical indexing
msgTable = struct2table(msg);

% Check which messages have the type 'error'
errorMatches = (strcmp(msgTable.Criticity, 'error'));

% Read the error messages to another table
errorMessage = msgTable(errorMatches, :);

Содержимое сообщения, возвращенного как вектор символов.

Пример: 'Start Extract user-implementation for Behavior ''pkg.tst002.swc001.bhv001''...'

Аналитический журнал, возвращенный как вектор символов.

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

Темы

Введенный в R2018b

Документация Polyspace Code Prover
Поддержка