デスクトップでの 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\bin の polyspace 実行可能ファイルをダブルクリックします。ここで、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');

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

その他の情報

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