メインコンテンツ

このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。

デスクトップでの PolyspaceCode Prover の実行

Polyspace® Code Prover™ は安定性の高い静的解析ツールで、C および C++ ソース コード内のオーバーフロー、ゼロ除算、配列の範囲外へのアクセスおよびその他特定のランタイム エラーの有無が証明されます。Code Prover 解析では、プログラムの実行、コード インストルメンテーションまたはテスト ケースを必要とすることなく、結果が生成されます。Code Prover では、セマンティクスの解析および形式的手法に基づく抽象的な解釈が使用され、コード内の制御フローおよびデータ フローが判断されます。Code Prover は、手書きのコード、生成されたコードまたはその 2 つの組み合わせに対して使用できます。解析結果では、各動作は色分けされ、ランタイム エラーなし、エラーと証明、到達不能、または未証明のいずれかであることが示されます。

Code Prover は、Polyspace ユーザー インターフェイスまたはスクリプトを使用して、C/C++ コードに対して実行できます。詳細は、以下を参照してください。

  • ユーザー インターフェイスでの Polyspace の実行

    Polyspace の使用が初めての場合は、Polyspace ユーザー インターフェイスから開始することができます。プロジェクトの設定ウィザード、構成の支援、解析ログの要約などの機能からヘルプを取得できます。

  • Windows または Linux コマンド ラインでの Polyspace の実行

    Polyspace ユーザー インターフェイスでプロジェクトを設定し、数回の試行を完了した後は、自動またはオンデマンドで実行するスクリプトに構成をエクスポートできます。オペレーティング システムのコマンド ラインから Polyspace 解析を直接実行することもできます。コマンドは後で実行するために、バッチ ファイル (Windows) またはシェル スクリプト (Linux) に保存することができます。Jenkins® などの継続的インテグレーション ツールを使用して Polyspace サーバー製品を実行している場合、Polyspace デスクトップ製品のスクリプトを再利用することができます。

  • MATLAB での Polyspace の実行

    MATLAB® をインストールしている場合は、スクリプトを書いて Polyspace 解析を実行することが特に簡単になります。たとえば、関数構文の自動ヘルプなど、MATLAB 環境におけるスクリプト作成のすべての利点を活用できます。解析後、MATLAB グラフィックスおよび可視化ツールを使用して、結果についての独自の可視化を作成できます。

例のファイル

このチュートリアルの手順に従うには、polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources からファイル example.c および include.h を別のフォルダーにコピーします。ここで、polyspaceroot は Polyspace インストール フォルダーです。たとえば、C:\Program Files\Polyspace\R2020a です。

ユーザー インターフェイスでの Polyspace の実行

Polyspace ユーザー インターフェイスを開く

polyspaceroot\polyspace\binpolyspace 実行可能ファイルをダブルクリックします。ここで、polyspaceroot は Polyspace インストール フォルダーです。たとえば、C:\Program Files\Polyspace\R2020a です。インストール フォルダーも参照してください。

デスクトップまたは Windows®[スタート] メニューに Polyspace へのショートカットを設定している場合は、そのショートカットをダブルクリックします。

ソース ファイルの追加

検証を実行するには、新しい Polyspace プロジェクトを作成する必要があります。Polyspace プロジェクトでは、ファイル システムのソース フォルダーとインクルード フォルダーを指し示します。

[スタート ページ] ペインの左側で、[新規プロジェクトの開始] をクリックします。あるいは、[ファイル][新規プロジェクト] を選択します。

プロジェクト名を指定したら、次の画面で、

  • ソース フォルダーを追加します。

    このチュートリアルでは、ファイル example.c を保存したフォルダーへのパスを追加します。[Next] をクリックします。

  • インクルード フォルダーを追加します。

    このチュートリアルでは、ファイル include.h を保存したフォルダーへのパスを追加します。このフォルダーは、前のフォルダーと同じにできます。[終了] をクリックします。

ソース フォルダーとインクルード フォルダーを追加し終わったら、[プロジェクト ブラウザー] ペインに新しいプロジェクトが表示されます。ソース フォルダーはプロジェクトの最初のモジュールにコピーされます。プロジェクトを右クリックし、後からフォルダーをさらに追加することができます。後からフォルダーを追加する場合は、そのフォルダーをモジュールに明示的にコピーしなければなりません。

Polyspace の設定と実行

Polyspace 解析に関連付けられている既定のオプションを変更できます。

プロジェクト モジュールで [構成] ノードをクリックします。必要に応じて、[構成] ペインでオプションを変更します。たとえば、[コーディング ルールおよびコード メトリクス] ノードで [MISRA C:2004 のチェック] を選択します。

詳細は、各オプションのツールヒントを参照してください。オプションの状況依存のヘルプについては、[詳しいヘルプ] リンクをクリックします。

検証を開始するには、上部のツール バーにある [Code Prover の実行] をクリックします。ボタンに Bug Finder が示されている場合は、ボタンの横の矢印をクリックして、Code Prover に切り替えます。

[出力の概要] ウィンドウで検証の進行状況を確認できます。検証後、結果が自動的に開きます。

その他の情報

詳細は、以下を参照してください。

Windows または Linux コマンド ラインでの Polyspace の実行

Windows または Linux® コマンド ラインから、バッチ (.bat) ファイルまたはシェル (.sh) スクリプトを使用して Code Prover を実行できます。

検証を実行するには polyspace-code-prover コマンドを使用します。

コマンドの絶対パスの入力を省略するために、パス polyspaceroot\polyspace\bin をオペレーティング システムの Path 環境変数に追加します。ここで、polyspaceroot は Polyspace インストール フォルダーです。たとえば、C:\Program Files\Polyspace\R2025a です。

(cd を使用して) ファイルを保存したフォルダーに移動します。以下を入力します。

polyspace-code-prover -sources example.c -I . -results-dir . -main-generator
ここで、. は現在のフォルダーを示します。使用されるオプションは以下のとおりです。

  • -sources:コンマ区切りのソース ファイルを指定します。

  • -I:インクルード フォルダーのパスを指定します。別のインクルード フォルダーを追加するたびに -I フラグを使用します。

  • -results-dir: Polyspace Code Prover の結果を保存するフォルダーへのパスを指定します。

    実行されるたびに結果フォルダーがクリーンアップされて再設定されることに注意してください。クリーンアップ中にファイルが誤って削除されないようにするには、他のファイルを含む既存のフォルダーを使用するのではなく、Polyspace の結果専用のフォルダーを指定します。

  • モジュールまたはライブラリの検証 (-main-generator):main 関数がソース ファイルにない場合に生成されなければならないことを指定します。

検証後、結果はファイル ps_results.pscp に保存されます。このファイルは Polyspace ユーザー インターフェイスから開くことができます。たとえば、以下を入力します。

polyspace ps_results.pscp

コマンド ラインでコンマ区切りのソースを直接指定する代わりに、テキスト ファイルにソースをリストできます (1 行につき 1 ファイル)。このテキスト ファイルを指定するには、オプション -sources-list-file を使用します。

その他の情報

詳細は、以下を参照してください。

MATLAB での Polyspace の実行

MATLAB から Polyspace を実行する前に、Polyspace インストールと MATLAB インストールをリンクしなければなりません。MATLAB や Simulink との Polyspace の統合を参照してください。

解析を実行するには、polyspace.Project オブジェクトを使用します。このオブジェクトには次の 2 つのプロパティがあります。

  • Configuration:このプロパティを使用して、ソース、インクルード、コンパイラ、結果フォルダーなどの解析オプションを指定します。

  • Results:このプロパティを使用して、解析後に解析結果を MATLAB table に読み取ります。

解析を実行するには、このオブジェクトの run メソッドを使用します。

polyspaceroot\polyspace\examples\cxx\Code_Prover_Examples\sources に含まれる例ファイル example.c に対して Polyspace を実行するには、MATLAB コマンド プロンプトに以下を入力します。

proj = polyspace.Project

% Configure analysis
proj.Configuration.Sources = {fullfile(polyspaceroot, 'polyspace', 'examples',...
    'cxx', 'Code_Prover_Example', 'sources', 'example.c')};
proj.Configuration.EnvironmentSettings.IncludeFolders = {fullfile(polyspaceroot,...
 'polyspace', 'examples', 'cxx', 'Code_Prover_Example', 'sources')};
proj.Configuration.TargetCompiler.Compiler = 'gnu4.9';
proj.Configuration.ResultsDir = fullfile(pwd,'results');
proj.Configuration.CodeProverVerification.MainGenerator = true;


% Run analysis
cpStatus = proj.run('codeProver');

% Read results
resObj = proj.Results;
cpSummary = getSummary(resObj, 'runtime');
cpResults = getResults(resObj, 'readable');

検証後、結果はファイル ps_results.pscp に保存されます。このファイルは Polyspace ユーザー インターフェイスから開くことができます。たとえば、以下を入力します。

resultsFile = fullfile(proj.Configuration.ResultsDir,'ps_results.pscp');
polyspaceCodeProver(resultsFile)

その他の情報

詳細は、以下を参照してください。

参考

トピック