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