Опции, чтобы управлять созданием проекта 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 и реализацию кода С только, но не запускайте анализ Code Prover. Используйте эту опцию во время обновлений проекта, чтобы исследовать ошибки, введенные в технических требованиях ARXML или ошибках компиляции, введенных в исходном коде. Можно сначала устранить эти проблемы, и затем запустить анализ Code Prover. |
Опции, чтобы управлять парсингом технических требований 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' | Разделенный пробелом список опций. | Задайте дополнительные опции для анализа Code Prover. Опции, которые вы задаете, не применяются к парсингу ARXML или экстракции кода, но только к последующему анализу Code Prover. Используйте этот метод, чтобы задать опции анализа, которые используются в non-AUTOSAR анализе Code Prover. См. Полный список Опций анализа Polyspace Code Prover. Например, вы можете хотеть задать компилятор и целевую архитектуру. По умолчанию компиляция проектов, созданных из технических требований 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. | Задайте дополнительные опции для анализа Code Prover в файле опций. Опции, которые вы задаете, не применяются к парсингу ARXML или экстракции кода, но только к последующему анализу Code Prover. Например, можно проследить команду сборки, чтобы собрать параметры компилятора, макроопределения и пути, чтобы включать папки и предоставить эту информацию в файле опций для анализа реализации кода компонентов программного обеспечения AUTOSAR.
Проследите свою команду сборки (например, make ) с polyspaceConfigure функционируйте и сгенерируйте файл опций для последующего анализа Code Prover. Подавите включение источников в файле опций с -no-sources опция. polyspaceConfigure -output-options-file options.txt -no-sources make Запустите Code Prover на коде AUTOSAR с polyspace-autosar . Обеспечьте свою папку ARXML, исходные папки и другие опции. Кроме того, предоставьте ранее сгенерированному файлу опций -extra-options-file опция. polyspaceAutosar(...,
'-extra-options-file','options.txt')
|
'-show-prove' | Полное полностью определенное имя поведения SWC, например, 'pkg.component.bhv' . | После анализа, открытых результатов для определенного компонента программного обеспечения, внутреннее поведение которого задано. |