MATLAB Coder によって生成された C/C++ コードの Polyspace 検証

MATLAB^® コードから生成された C/C++ コードのランタイムエラーをチェックするには、Polyspace^® Code Prover™ を使用できます。欠陥をチェックするには、Polyspace Bug Finder™ を使用できます。Polyspace と Embedded Coder^® を使用している場合、Polyspace は MATLAB Coder™ ワークフローに統合されます。

MATLAB Coder アプリでは、追加の設定を行わずに Polyspace 解析を実行できます。
コマンドラインでは、codegen によるコード生成後に、pslinkrun (Polyspace Bug Finder) にコード生成出力フォルダーを指定することで、生成されたコードに対して Polyspace 解析を実行できます。

MATLAB Coder アプリでの Polyspace 解析の実行

スタンドアロン C/C++ コード (スタティックライブラリ、ダイナミックリンクライブラリ、または実行可能プログラム) を生成します。
[コード生成] ページで [Polyspace] をクリックします。
オプションを選択します。MATLAB Coder アプリでの Polyspace 詳細オプションの設定 (Polyspace Code Prover)を参照してください。
[実行] をクリックします。
[Polyspace のログ] タブに解析出力のログが記録され、Polyspace ユーザーインターフェイスが開きます。

`codegen` によって生成されたコードに対する Polyspace 解析の実行

MATLAB Coder によって生成されたコードを検証するための pslinkoptions オブジェクトを作成します。
必要に応じて、オブジェクトプロパティを変更します。
- ResultDir プロパティで、Polyspace の結果用フォルダーの名前を指定します。
- VerificationMode プロパティで、Polyspace 検証製品を指定します。
pslinkrun を使用して検証を実行します。pslinkoptions オブジェクトと、生成コードが含まれるフォルダーを指定します。
検証結果を表示するには、Polyspace ユーザーインターフェイスを開きます。

たとえば、MATLAB 関数 myFunction のスタティックライブラリを生成しており、コード生成出力フォルダーが codegen/lib/myFunction であるとします。生成されたコードに対して Polyspace Code Prover を実行するには、次のコードを使用します。

opts = pslinkoptions('codegen');
opts.ResultDir = 'polyspace';
opts.VerificationMode = 'CodeProver';
pslinkrun('-codegenfolder', 'codegen/lib/myFunction', opts);
polyspaceCodeProver('polyspace/myFunction.psprj');

VerificationMode プロパティを 'BugFinder' に設定し、polyspaceBugFinder を使用して検証結果を表示することもできます。

解析結果の確認

Polyspace ユーザーインターフェイスの [検証結果のリスト] ペインで、実行時チェックを確認します。問題から元の MATLAB コードにトレースできるかどうかを確認します。Interactively Trace Between MATLAB Code and Generated C/C++ Codeを参照してください。

たとえば、Polyspace では関数入力の範囲が無制限であるとみなされるため、C コードの演算がオーバーフローする可能性があります。入力に対して制約を指定し、Polyspace でコードを再解析することを検討してください。MATLAB コードから生成された C/C++ コードに対する Polyspace の実行 (Polyspace Code Prover)を参照してください。

参考

pslinkoptions (Polyspace Code Prover) | pslinkrun (Polyspace Code Prover)