このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。
polyspaceCodeProver
Polyspace Code Prover 検証を MATLAB から実行
スクリプト化を容易にするには、polyspace.Project オブジェクトを使用して Polyspace® 解析を実行します。
構文
説明
polyspaceCodeProver は、Polyspace Code Prover™ を開きます。
status = polyspaceCodeProver(projectFile)
status = polyspaceCodeProver(optsObject)
メモ
Polyspace オプション オブジェクトを使用して解析を実行する場合、解析のオプションの指定には Polyspace オプション オブジェクトのみを使用します。1 番目の引数が Polyspace オプション オブジェクトの場合、名前と値の引数の使用はサポートされていません。
status = polyspaceCodeProver(projectFile, '-nodesktop')
status = polyspaceCodeProver(resultsFile)
status = polyspaceCodeProver('-results-dir',resultsFolder)resultsFolder の Polyspace の結果ファイルを Polyspace Code Prover で開きます。
status = polyspaceCodeProver('-help')polyspaceCodeProver コマンドに指定できるすべてのオプションを表示します。
status = polyspaceCodeProver('-sources',sourceFiles)sourceFiles で指定されたソース ファイルで Polyspace Code Prover 検証を実行します。
polyspaceCodeProver('-sources', は、1 つ以上の sourceFiles,Name,Value)Name,Value ペア引数で指定される追加オプションを使用して、Polyspace Code Prover 検証をソース ファイルに対して実行します。
メモ
MATLAB から Polyspace を実行する前に、Polyspace インストールと MATLAB インストールをリンクしなければなりません。MATLAB や Simulink との Polyspace の統合を参照してください。
[ は、解析の負荷をリモート クラスターに移します。ここで、status, jobID] = polyspaceCodeProver(___,'-batch','-scheduler',scheduler)scheduler は、複数のクライアントからの解析の送信を管理する、クラスターのヘッド ノードを示します。クラスター内の 2 つのジョブを操作も参照してください。
例
MATLAB から Polyspace プロジェクトを開く
この例では、拡張子 .psprj をもつ Polyspace プロジェクト ファイルを MATLAB から開く方法を示します。この例では、プロジェクト ファイル Code_Prover_Example.psprj を開きます。
プロジェクト ファイルへの絶対パスを MATLAB 変数 prjFile に代入します。
prjFile = fullfile(polyspaceroot, 'polyspace', 'examples', 'cxx', ... 'Code_Prover_Example', 'Code_Prover_Example.psprj');
プロジェクトを開きます。
polyspaceCodeProver(prjFile)
MATLAB から Polyspace の結果を開く
この例では、Polyspace の結果ファイルを MATLAB から開く方法を示します。この例では、結果ファイルをフォルダー polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\Module_1\CP_Result
フォルダーの絶対パスを MATLAB 変数 resFolder に代入します。
resFolder = fullfile(polyspaceroot, 'polyspace', 'examples', ... 'cxx', 'Code_Prover_Example', 'Module_1', 'CP_Result');
結果を開きます。
polyspaceCodeProver('-results-dir',resFolder)オプション オブジェクトを使用した Polyspace 検証の実行
この例では、オブジェクトを使用して MATLAB で Polyspace 検証を実行する方法を示します。
オプション オブジェクトを作成し、ソース ファイルとインクルード フォルダーをプロパティに追加します。
opts = polyspace.Options;
opts.Sources = {fullfile(polyspaceroot, 'polyspace', 'examples',...
'cxx', 'Code_Prover_Example', 'sources', 'single_file_analysis.c')};
opts.EnvironmentSettings.IncludeFolders = {fullfile(polyspaceroot, 'polyspace', 'examples',...
'cxx', 'Code_Prover_Example', 'sources')};
opts.ResultsDir = fullfile(pwd,'results');検証を実行し、結果を表示します。
polyspaceCodeProver(opts);
polyspaceCodeProver('-results-dir',opts.ResultsDir)DOS/UNIX のオプションを使用した MATLAB からの Polyspace 検証の実行
この例では、DOS/UNIX スタイルのオプションを使用して MATLAB で Polyspace 検証を実行する方法を示します。
解析を実行し、結果を開きます。
sourceFiles = fullfile(polyspaceroot, 'polyspace', 'examples',... 'cxx', 'Code_Prover_Example', 'sources', 'single_file_analysis.c'); includeFolders = fullfile(polyspaceroot, 'polyspace', 'examples',... 'cxx', 'Code_Prover_Example', 'sources'); resultsDir = fullfile(pwd,'results'); polyspaceCodeProver('-sources',sourceFiles, ... '-I',includeFolders, ... '-results-dir',resultsDir,... '-main-generator'); polyspaceCodeProver('-results-dir',resultsDir);
コーディング ルールのチェックを伴う Polyspace 検証を実行
この例では、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.MisraC3Subset = 'mandatory'; opts.CodingRulesCodeMetrics.EnableMisraC3 = true; opts.CodeProverVerification.EnableMain = true; opts.InputsStubbing.DoNotGenerateResultsFor = 'all-headers'; polyspaceCodeProver(opts); polyspaceCodeProver('-results-dir',resFolder1);
DOS/UNIX のオプションを使用してコーディング ルールを検証します。
polyspaceCodeProver('-sources',sourceFileName,... '-I',includeFileName, ... '-results-dir',resFolder2,... '-misra3','mandatory',... '-do-not-generate-results-for','all-headers',... '-main-generator'); polyspaceCodeProver('-results-dir',resFolder2);
入力引数
名前と値の引数
出力引数
バージョン履歴
R2013b で導入
