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