Main Content

分散ワークフローでスタンドアロン コードとして生成されたコードの解析

関数 polyspacepackNGo を使用して Simulink® モデルから Polyspace® オプション ファイルを生成してパッケージ化します。これらのオプション ファイルを使用して、設計範囲指定などのモデル固有の情報を使用する生成されたコードについて、Simulink を必要とすることなく Polyspace 解析を実行します。

モデルを開く

モデル demo_math_operations は、モデルの入力に対してさまざまな数学演算を実行します。モデルにはカスタムの C コードを実行する C Function ブロックがあります。モデルには C 関数 GMean を呼び出す C Caller ブロックもあります。これはソース ファイル GMean.c で実装されています。コード生成と Polyspace オプション ファイルのパッケージ化のためにモデルを開くには、MATLAB ヘルプ ブラウザーで現在のトピックを検索し、[モデルを開く] ボタンをクリックします。または、MATLAB コマンド ウィンドウで、次のコードを貼り付けて実行します。

openExample('simulink_general/PPNGStandAloneExample');
open_system('demo_math_operations');

モデルの設定

コードの生成と Polyspace オプション ファイルのパッケージ化のためにモデルを構成するには、次のコンフィギュレーション パラメーターを指定します。

  • 生成されるコードを含むアーカイブを作成するには、'PackageGeneratedCodeAndArtifacts'true に設定します。

  • コード アーカイブの名前を指定します。たとえば、名前を genCodeArchive.zip に設定します。

  • コード生成中に [シミュレーション ターゲット] で指定されたカスタム コード設定を使用するには、'RTWUseSimCustomCode''on' に設定します。

  • モデルと生成されたコードが Polyspace と互換性があるようにするには、ert.tlc をシステム ターゲット ファイルとして設定します。Polyspace 解析で推奨されるモデル コンフィギュレーション パラメーター (Polyspace Bug Finder)を参照してください。

コマンド ウィンドウまたはエディターで次のパラメーター構成を入力します。

configSet = getActiveConfigSet('demo_math_operations');
set_param(configSet, 'PackageGeneratedCodeAndArtifacts', true);
set_param(configSet, 'PackageName', 'genCodeArchive.zip');
set_param(configSet, 'SystemTargetFile', 'ert.tlc');
set_param(configSet,'RTWUseSimCustomCode','on')

コード アーカイブの生成

生成されたコードを格納するフォルダーを指定します。コード生成を開始するには、コマンド ウィンドウまたはエディターで次のように入力します。

codegenFolder = 'demo_math_operations_ert_rtw';
if exist(fullfile(pwd,codegenFolder), 'dir') == 0
    slbuild('demo_math_operations')
end

PackageGeneratedCodeAndArtifactstrue に設定されているため、生成されたコードはアーカイブ genCodeArchive.zip に挿入されます。

Polyspace オプション ファイルの生成とパッケージ化

生成されたコード向けの Polyspace オプションを生成するには、コマンド ウィンドウまたはエディターで次のように入力します。

zipFile = polyspacePackNGo('demo_math_operations');

アーカイブ genCodeArchive.zip で、フォルダー <current folder>/polyspace でオプション ファイルを見つけます。

パッケージ化されたオプション ファイルを使用した Polyspace 解析の実行

  1. コード アーカイブ genCodeArchive.zip を解凍して <current folder>/polyspace フォルダーを見つけます。

  2. コマンド ライン ターミナルを開いて、cd コマンドを使用して、解凍されたフォルダーの polyspace サブフォルダーに作業フォルダーを変更します。

  3. Polyspace 解析を開始します。

    • デスクトップ Polyspace 解析を実行するには、polyspace-code-prover または polyspace-bug-finder のいずれかを使用します。サーバーで Polyspace 解析を実行するには、polyspace-bug-finder-server または polyspace-code-prover-server のいずれかを使用します。Polyspace の Bug Finder と Code Prover とではコードの解析方法が異なります。Polyspace Bug Finder と Polyspace Code Prover の違い (Polyspace Bug Finder)を参照してください。

    • ファイル optionsFile.txt-options-file の引数として指定します。

    Code Prover 解析を実行するには次のコマンドを実行します。polyspace-code-prover -options-file optionsFile.txt -results-dir Results

  4. Results フォルダーに生成されるログ ファイルで解析の進行状況を確認します。

  5. デスクトップ ユーザー インターフェイスで結果を表示するには、コマンド ライン インターフェイスで次を入力します。polyspace Results\ps_results.pscpps_results ファイルの拡張子は、実行するのが Code Prover 解析か Bug Finder 解析かによって変わります。結果にはさまざまなオレンジ チェックが含まれます。

    または、結果を Polyspace Access にアップロードします。検証結果を Polyspace Access にアップロード (Polyspace Bug Finder)を参照してください。

  6. 結果を確認します。詳細については、バグ修正またはコメントによる検証結果への対処 (Polyspace Bug Finder)を参照してください。

参考

| | (Embedded Coder)