ビルド コマンドを使用した AUTOSAR コードに対する Polyspace の実行
このトピックでは、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 が認識するようになったため、コンパイル エラーが表示されなくなります。
