polyspaceCodeProverServer

Polyspace Code Prover 検証を MATLAB から実行

ページ内をすべて折りたたむ

スクリプト化を容易にするには、polyspace.Project オブジェクトを使用して Polyspace® 解析を実行します。

構文

polyspaceCodeProverServer(optsObject)
polyspaceCodeProverServer('-help')
polyspaceCodeProverServer('-sources',sourceFiles)
polyspaceCodeProverServer('-sources',sourceFiles,Name,Value)

説明

polyspaceCodeProverServer(optsObject) では、Polyspace オプション オブジェクトに対して、MATLAB® で検証が実行されます。

例

polyspaceCodeProverServer('-help') は、Polyspace Code Prover™ 検証を実行するために polyspaceCodeProverServer コマンドに指定できるすべてのオプションを表示します。

polyspaceCodeProverServer('-sources',sourceFiles) は、sourceFiles で指定されたソース ファイルで Polyspace Code Prover 検証を実行します。

例

polyspaceCodeProverServer('-sources',sourceFiles,Name,Value) は、1 つ以上の Name,Value ペア引数で指定される追加オプションを使用して、Polyspace Code Prover 検証をソース ファイルに対して実行します。

メモ

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

例

例

すべて折りたたむ

この例では、Polyspace 検証を MATLAB コマンド ラインから実行する方法を示します。この例では次のようになります。

  • ディレクトリ polyspaceroot/polyspace/examples/cxx/BugFinder_example/sources にあるソース ファイル numerical.c を使用する。

  • 同じディレクトリにあるヘッダーをインクルードする。

オプション オブジェクトを作成し、ソース ファイルとインクルード フォルダーをプロパティに追加します。

opts = polyspace.Options;
opts.Sources = {fullfile(polyspaceroot, 'polyspace', 'examples',...
    'cxx', 'Bug_Finder_Example', 'sources', 'numerical.c')};;
opts.EnvironmentSettings.IncludeFolders = {fullfile(polyspaceroot, 'polyspace', 'examples',...
    'cxx', 'Bug_Finder_Example', 'sources')};
opts.ResultsDir = 'C:\Polyspace_Results';

解析を実行して結果を表示します。

polyspaceCodeProverServer(opts);

Code Prover 解析はファイル C:\Polyspace_Sources\source.c に対して検証を実行し、結果を C:\Polyspace_Results に保存します。

この例では、DOS/UNIX のオプションを使用して単一ソース ファイルに対して Polyspace 検証を実行する方法を示します。この例では次のようになります。

  • ディレクトリ polyspaceroot/polyspace/examples/cxx/BugFinder_example/sources にあるソース ファイル numerical.c を使用する。

  • 同じディレクトリにあるヘッダーをインクルードする。

ソース ファイルとインクルード ファイルの場所を定義します。

src = fullfile(polyspaceroot, 'polyspace', 'examples',...
    'cxx', 'Bug_Finder_Example', 'sources', 'numerical.c');
inc = fullfile(polyspaceroot, 'polyspace', 'examples',...
    'cxx', 'Bug_Finder_Example', 'sources');
res = fullfile(pwd,'results');

検証を実行し、結果を開きます。

polyspaceCodeProverServer('-sources',src, ...
    '-I',inc, ...
    '-results-dir',res)

この例では、MATLAB で検証をカスタマイズする 2 つの異なる方法を示します。オプション オブジェクトのプロパティを変更するか、名前と値のペアを使用することで、追加オプションをいくつでもカスタマイズできます。MISRA C™ 2012 コーディング ルールのチェックからヘッダーを除外して、コーディング ルールのチェックを指定し、main を生成します。

ソース ファイル パス用の変数を作成する場合、いずれかの解析手法で使用するフォルダーのパスと結果フォルダーのパスを含めます。

sourceFileName = fullfile(polyspaceroot, 'polyspace','examples', 'cxx', 'Code_Prover_Example','sources','example.c');
includeFileName = fullfile(polyspaceroot, 'polyspace','examples', 'cxx', 'Code_Prover_Example','sources','include.h');
resFolder1 = fullfile('Polyspace_Results_1');
resFolder2 = fullfile('Polyspace_Results_2');

オプション オブジェクトを使用してコーディング ルールを検証します。

opts = polyspace.Options('C');
opts.Sources = {sourceFileName};
opts.EnvironmentSettings.IncludeFolders = {includeFileName};
opts.ResultsDir = resFolder1;
opts.CodingRulesCodeMetrics.EnableMisraC3 = true;
opts.CodingRulesCodeMetrics.MisraC3Subset = 'mandatory';
opts.CodeProverVerification.EnableMain = true;
opts.InputsStubbing.DoNotGenerateResultsFor = 'all-headers';
polyspaceCodeProverServer(opts);

DOS/UNIX のオプションを使用してコーディング ルールを検証します。

polyspaceCodeProverServer('-sources',sourceFileName,...
     '-I',includeFileName, ...
     '-results-dir',resFolder2,...
     '-misra3','mandatory',...
     '-do-not-generate-results-for','all-headers',...
     '-main-generator');

入力引数

すべて折りたたむ

Polyspace オプション オブジェクト名をオブジェクト ハンドルとして指定します。

オプション オブジェクトを作成するには、Polyspace オプションのクラス polyspace.Options または polyspace.Project を使用します。

例: opts

拡張子 .c または .cpp をもつソース ファイルの、コンマで区切られた名前。単一文字ベクトルとして指定します。

ファイルが現在のフォルダーに存在しない場合、sourceFiles は絶対パスまたは相対パスを含んでいなければなりません。

例: 'myFile.c', 'C:\mySources\myFile1.c,C:\mySources\myFile2.c'

名前と値の引数

オプションの引数のペアを Name1=Value1,...,NameN=ValueN として指定します。ここで、Name は引数名で、Value は対応する値です。名前と値の引数は他の引数の後に指定しなければなりませんが、ペアの順序は重要ではありません。

R2021a より前では、コンマを使用して名前と値をそれぞれ区切り、Name を引用符で囲みます。

例: '-target','i386','-compiler','gnu4.6' は、ソース コードが i386 プロセッサを対象とし、GCC 4.6 コンパイラの非 ANSI C 構文を含んでいることを指定します。

すべての解析オプションのリストは、すべての Polyspace Code Prover 解析オプションのリストを参照してください。

バージョン履歴

R2019a で導入

参考

トピック