ビルド コマンドを使用した AUTOSAR コードに対する Polyspace の実行

R2026b

このトピックでは、Polyspace® でのコンポーネント ベースの AUTOSAR コード検証方法について説明します。統合解析方法については、Polyspace で AUTOSAR コードのコンポーネント ベースの解析と統合解析のどちらかを選択するを参照してください。

ソフトウェア開発に AUTOSAR の方法論を使用し、コンパイルにビルド コマンドを使用する場合、既存のアーティファクトを再利用して Code Prover にソース ファイルとコンパイル オプションを指定できます。

  • AUTOSAR XML ファイルのソース ファイル仕様を再利用できます。

    Polyspace では、AUTOSAR XML 仕様を読み取って、各ソフトウェア コンポーネントに関連するソース ファイルを、以降の Code Prover 実行時チェックの対象となるプロジェクトに抽出します。ソフトウェア開発に AUTOSAR の方法論を使用する場合、この方法論に組み込まれたモジュール化をモジュラー Code Prover 解析に再利用できます。polyspace-autosar を参照してください。

  • ビルド コマンドで指定したコンパイル オプションを再利用できます。

    Polyspace では、ビルド コマンドをトレースして、標準のインクルードやマクロ定義へのパスなどのコンパイル オプションと共に呼び出されるコンパイラを検出できます。polyspace-configure を参照してください。

このトピックでは、2 つの方法を組み合わせて、Code Prover 解析を自動化する方法を説明します。

例のファイル

このチュートリアルの手順に従うには、polyspaceroot/polyspace/examples/doc_cxx/polyspace_autosar_configure に含まれるデモ ファイルを使用します。

この例では、Linux ベースの makefile と Linux® のパスの区切り記号を使用します。例を Windows® で実行するには、適切な変更を加えます。

コンパイル オプションを使用しない Code Prover の実行

デモ フォルダーのコンテンツを /tmp/demo/ などの一時フォルダーにコピーします。そのフォルダーに移動します。

cd /tmp/demo

サブフォルダー mRtwDemoAutosar_autosar_rtw に含まれる ARXML ファイルとソース ファイルに対して Code Prover を実行します。結果をフォルダー /tmp/res に保存します。

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

コンパイル エラーに注目します。たとえば、/tmp/res/.extract フォルダーで、ファイル GPIO_read.log を開きます。マクロ MY_DEFINE_FROM_SIMULINK が定義されていないため、#error 命令が表示されます。

/tmp/demo/mRtwDemoAutosar_autosar_rtw のファイル GPIO_read.c を開くと、問題の原因となっている行がわかります。

#ifndef MY_DEFINE_FROM_SIMULINK
#error Missing MY_DEFINE_FROM_SIMULINK
#endif

この行は、マクロ MY_DEFINE_FROM_SIMULINK が定義されない限り、前処理中にエラーを引き起こすと想定されます。

ビルド コマンドのコンパイル オプションを使用した Code Prover の実行

/tmp/demo/mRtwDemoAutosar_autosar_rtw の makefile mRtwDemoAutosar.mk は、マクロと、インクルード フォルダーへのパスを定義しています。たとえば、以前に不足していたマクロ MY_DEFINE_FROM_SIMULINK は次の行で定義されています。

DEFINES_CUSTOM = -DMY_DEFINE_FROM_SIMULINK

makefile を含むフォルダーに移動します。

cd /tmp/demo/mRtwDemoAutosar_autosar_rtw

この makefile mRtwDemoAutosar.mk を使用するビルド コマンドからコンパイル オプションを抽出します。たとえば、MATLAB® を /usr/local/MATLAB/R2018b にインストールした場合、以下のように makefile をトレースできます。

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

makefile に含まれるコンパイル オプションは Polyspace 解析オプションに変換され、オプション ファイル psoptions に保存されます。-no-sources オプションは、polyspace-configure コマンドがコンパイル オプションのみを抽出し、ソースは抽出しないようにします。START_DIR と MATLAB_ROOT は、デモ makefile に固有の変数で、使用する他の makefile では必要ない可能性があります。

polyspace-autosar コマンドの以前の実行から結果を削除します。

rm -r /tmp/res

前の手順で作成したオプション ファイル psoptions を polyspace-autosar コマンドに指定します。

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

ビルド コマンドで使用したコンパイル オプションを Code Prover が認識するようになったため、コンパイル エラーが表示されなくなります。

参考

トピック