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

polyspace-code-prover

(システム コマンド) Windows、Linux、またはその他のコマンド ラインから Code Prover 検証を実行

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

構文

polyspace-code-prover [options]
polyspace-code-prover -sources sourceFiles [options]
polyspace-code-prover -sources-list-file listOfSources [options]
polyspace-code-prover -options-file optFile
polyspace-code-prover -h[elp]

説明

polyspace-code-prover システム コマンドは、コマンド ラインで、コマンド ライン フラグとして指定された解析オプション、またはオプション ファイルを使用して Polyspace® Code Prover™ 解析を実行します。

メモ

この Polyspace コマンドは polyspaceroot\polyspace\bin にあります。ここで、polyspaceroot は Polyspace インストール フォルダー (C:\Program Files\Polyspace\R2025a など) です (インストール フォルダーも参照してください)。コマンドの絶対パスの入力を省略するには、この場所をオペレーティング システムの PATH 環境変数に追加します。

polyspace-code-prover [options] は、現在のフォルダーに、ソース ファイル (.c ファイルまたは .cxx ファイル) が含まれた sources サブフォルダーがある場合に、Code Prover 検証を実行します。この検証では、sources 内のファイルと、sources の下にあるすべてのサブフォルダーが考慮されます。この検証は追加オプションを使用してカスタマイズできます。

polyspace-code-prover -sources sourceFiles [options] は、ソース ファイル sourceFiles に対して Code Prover 検証を実行します。この検証は追加オプションを使用してカスタマイズできます。

例

polyspace-code-prover -sources-list-file listOfSources [options] は、テキスト ファイル listOfSources にリストされたソース ファイルに対して Code Prover 検証を実行します。この検証は追加オプションを使用してカスタマイズできます。

polyspace-code-prover -options-file optFile は、オプション ファイルで指定されたオプションを使用して Code Prover 検証を実行します。

例

polyspace-code-prover -h[elp] は使用可能な解析オプションの概要をリストします。

例

すべて折りたたむ

コマンド自体で解析オプションを指定して、ローカル Code Prover 検証を実行します。この例では、Polyspace Code Prover のデモ例にあるソース ファイルを使用します。この例を実行するには、polyspaceroot を Polyspace インストールのパス (C:\Program Files\Polyspace\R2025a など) に置き換えます。

MISRA C:2012 必須ルールをチェックと GNU 4.7 コンパイラ設定を使用して、numerical.c と programming.c で検証を実行します。次の例のコマンドは、可読性のために ^ 文字で分割しています。実際は、すべてのコマンドを 1 行に配置できます。

polyspace-code-prover -lang C^
 -sources polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources\*.c,^
 -I polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources\^
 -compiler generic -misra3 mandatory^
 -author jlittle -prog myProject -results-dir C:\Polyspace_Workspace\Results\

結果を開きます。

polyspace C:\Polyspace_Workspace\Results\ps_results.pscp

検証を再実行する場合は、コマンド ラインから再実行しなければなりません。

オプション ファイルを使用してソース ファイルと解析オプションを指定し、検証を実行します。この例を実行するには、polyspaceroot を Polyspace インストールのパス (C:\Program Files\Polyspace\R2025a など) に置き換えます。

次のテキストを、テキスト ファイル myOptsFile.txt に保存します。

# Polyspace analysis options 
-I polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources
-verif-version 1.0
-sources polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources\*.c
-lang C
-target i386
-compiler generic
-dos
-do-not-generate-results-for all-headers
-misra3 mandatory-required
-entry-points proc1,proc2,server1,server2,tregulate
-critical-section-begin Begin_CS:Cs10
-critical-section-end End_CS:Cs10
-temporal-exclusions-file polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources\temporal_exclusions.txt
-float-rounding-mode to-nearest
-signed-integer-overflows forbid
-unsigned-integer-overflows allow
-uncalled-function-checks none
-check-subnormal allow
-O2
-to Software Safety Analysis level 2
-context-sensitivity-auto
-path-sensitivity-delta 0
-author jlittle 
-prog myProject 
-results-dir C:\Polyspace_Workspace\Results\

テキスト ファイルで指定したオプションを使って検証を実行します。

polyspace-code-prover -options-file myOptsFile.txt

結果を開きます。

polyspace C:\Polyspace_Workspace\Results\ps_results.pscp

検証を再実行する場合は、コマンド ラインから再実行しなければなりません。

入力引数

すべて折りたたむ

C または C++ のコンマ区切りのソース ファイル名を文字列として指定します。ファイルが現在のフォルダー (pwd) に存在しない場合、sourceFiles は絶対パスまたは相対パスを含んでいなければなりません。スペースを含むパスによるエラーを避けるために、パスを引用符 " " で囲みます。詳細は、-sourcesを参照してください。

現在のフォルダーに、ソース ファイルが含まれた sources サブフォルダーがある場合、-sources フラグを省略できます。この検証では、sources 内のファイルと、sources の下にあるすべてのサブフォルダーが考慮されます。

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

C または C++ のファイル名をリストするテキスト ファイルを文字列として指定します。ファイルが現在のフォルダー (pwd) に存在しない場合、listOfSources は絶対パスまたは相対パスを含んでいなければなりません。スペースを含むパスによるエラーを避けるために、パスを引用符 " " で囲みます。詳細は、-sources-list-fileを参照してください。

例: filename.txt, "C:\ps_analysis\source_files.txt"

解析オプションと対応する値を、オプション名と該当する場合はその値によって指定します。構文の指定は、個々の解析オプションのリファレンス ページを参照してください。

例: -lang C-CPP, -target i386

解析オプションと値をリストするテキスト ファイルを文字列として指定します。詳細は、-options-fileを参照してください。

例: opts.txt, "C:\ps_analysis\options.txt"

ヒント

このコマンドをスクリプトの一部として実行する場合は、終了ステータスを調べて、解析が正常に完了したことを確認します。このコマンドは、解析が正常に完了するとゼロを返します。非ゼロの戻り値は、分析が失敗して完了しなかったことを意味します。たとえば、解析対象のファイルがコンパイルされない場合、このコマンドは非ゼロの値を返します。複数のファイルの解析中に一部のファイルがコンパイルされない場合、このコマンドはコンパイルされたファイルの解析を完了して、ゼロを返します。ファイルがコンパイルされない場合は解析を停止することが可能です。ファイルがコンパイルされない場合は解析を停止 (-stop-if-compile-error)を参照してください。

コマンドの実行後、Windows コマンド ラインで変数 %ERRORLEVEL% を調べて、解析が正常に完了したことを確認できます。

バージョン履歴

R2013b で導入

参考

トピック