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

Эта тема описывает компонентно-ориентированный подход к проверке кода AUTOSAR с Polyspace. Для аналитического подхода интегрирования смотрите, Выбирают Between Component-Based и Integration Analysis of AUTOSAR Code with Polyspace.

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

  • Можно снова использовать спецификацию исходного файла в XML-файлах AUTOSAR.

    Polyspace® может считать спецификации XML AUTOSAR и извлечь исходные файлы, вовлеченные в каждый компонент программного обеспечения в модули для последующих проверок на этапе выполнения Программы автоматического доказательства Кода. Если вы используете методологию AUTOSAR для разработки программного обеспечения, можно снова использовать модуляризацию, встроенную в эту методологию для модульного анализа Программы автоматического доказательства Кода. Смотрите polyspace-autosar.

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

    Polyspace может проследить вашу команду сборки и обнаружить компилятор, вызванный наряду с параметрами компиляции, такими как пути к стандарту, включает и макроопределения. Смотрите polyspace-configure.

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

Чтобы выполнить шаги в этом примере, используйте демонстрационные файлы в polyspaceroot/help/toolbox/codeprover/examples/polyspace_autosar_configure.

Пример использует основанный на Linux make-файл и диафрагмы пути Linux. Чтобы запустить пример в Windows®, сделайте соответствующие модификации.

Запустите программу автоматического доказательства кода без параметров компиляции

Скопируйте содержимое демонстрационной папки во временную папку, например, /tmp/demo/. Перейдите к той папке.

cd /tmp/demo

Запустите Программу автоматического доказательства Кода на ARXML и исходных файлах в подпапке mRtwDemoAutosar_autosar_rtw. Сохраните результаты в папке /tmp/res.

polyspace-autosar -create-project /tmp/res \
-arxml-dir mRtwDemoAutosar_autosar_rtw \
-sources-dir mRtwDemoAutosar_autosar_rtw

Отметьте ошибки компиляции. Например, в /tmp/res/.extract папка, откройте файл GPIO_read.log. Вы видите #error директива, потому что макро-MY_DEFINE_FROM_SIMULINK не задан.

Если вы открываете файл GPIO_read.c в /tmp/demo/mRtwDemoAutosar_autosar_rtw, вы видите, что линия вызывает проблему.

#ifndef MY_DEFINE_FROM_SIMULINK
#error Missing MY_DEFINE_FROM_SIMULINK
#endif

Эта линия, как предполагается, вызывает ошибку во время предварительной обработки если макро-MY_DEFINE_FROM_SIMULINK задан.

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

Make-файл mRtwDemoAutosar.mk в /tmp/demo/mRtwDemoAutosar_autosar_rtw задает макросы и пути, чтобы включать папки. Например, ранее недостающий макро-MY_DEFINE_FROM_SIMULINK задан в линии:

DEFINES_CUSTOM = -DMY_DEFINE_FROM_SIMULINK

Перейдите к папке, содержащей make-файл.

cd /tmp/demo/mRtwDemoAutosar_autosar_rtw

Извлеките параметры компиляции из команды сборки, которая использует этот make-файл mRtwDemoAutosar.mk. Например, если вы установили MATLAB® в /usr/local/MATLAB/R2018b, можно проследить make-файл как это.

polyspace-configure -no-sources \
-output-options-file psoptions -allow-overwrite\
make -B -f mRtwDemoAutosar.mk START_DIR=.. \
MATLAB_ROOT=/usr/local/MATLAB/R2018b buildobj

Параметры компиляции в make-файле преобразованы в опции анализа Polyspace и сохраненные в файле опций psoptions. -no-sources опция гарантирует что polyspace-configure команда извлекает параметры компиляции только и не источники. START_DIR и MATLAB_ROOT переменные, характерные для демонстрационного make-файла, и не могут требоваться в других make-файлах, которые вы используете.

Удалите результаты любого предыдущего запуска polyspace-autosar команда.

rm -r /tmp/res

Предоставьте файлу опций psoptions созданный на предыдущем шаге к polyspace-autosar команда.

polyspace-autosar -create-project /tmp/res \
-arxml-dir . \
-sources-dir .\
-extra-options-file psoptions

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

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

Похожие темы