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