コマンドラインからの Polyspace 解析の実行

DOS または UNIX^® のコマンドウィンドウから解析を実行するには、コマンド polyspace-bug-finder または polyspace-code-prover を使用し、使用する他のオプションをその後に続けます。参考:

polyspace-bug-finder
polyspace-code-prover (Polyspace Code Prover)

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

ソースおよび解析オプションの直接指定

Windows^®、Linux^®、または Mac OS X のコマンドラインで、ソースと解析オプションを polyspace-bug-finder または polyspace-code-prover コマンドに追加します。

次に例を示します。

ソースを指定するには、-sources オプションを使用し、コンマ区切りのソースのリストをその後に続けます。
```
polyspace-bug-finder -sources C:\mySource\myFile1.c,C:\mySource\myFile2.c
```
現在のフォルダーに、ソースファイルが含まれた sources サブフォルダーがある場合、-sources フラグを省略できます。この解析では、sources 内のファイルと、sources の下にあるすべてのサブフォルダーが考慮されます。
ターゲットプロセッサを指定するには、-target オプションを使用します。たとえば、ソースファイル file.c に対して m68k プロセッサを指定するには、次のコマンドを使用します。
```
polyspace-bug-finder -sources "file.c" -lang c -target m68k
```
MISRA C™ ルールに対する違反をチェックするには、-misra2 オプションを使用します。たとえば、ソースファイル file.c で必要な MISRA C ルールのみをチェックする場合は、次のコマンドを使用します。
```
polyspace-bug-finder -sources "file.c" -misra2 required-rules
```
結果フォルダーを指定するには、オプション -results-dir を使用します。
既定では、実行されるたびに結果フォルダーがクリーンアップされて再設定されることに注意してください。クリーンアップ中にファイルが誤って削除されないようにするには、他のファイルを含む既存のフォルダーを使用するのではなく、Polyspace^® の結果専用のフォルダーを指定します。

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

すべてのオプションのリストを確認するには、コマンドラインで次のように入力します。

polyspace-bug-finder -help

テキストファイルでのソースおよび解析オプションの指定

オプションを直接指定する代わりに、テキストファイルにオプションを保存して、解析を実行するたびにそのテキストファイルを使用することができます。

オプションを入れた listofoptions.txt と呼ばれるオプションファイルを作成します。次に例を示します。

#These are the options for MyCodeProverProject
-lang c
-prog MyCodeProverProject
-author jsmith
-sources "mymain.c,funAlgebra.c,funGeometry.c"
-target x86_64
-compiler generic
-dos
-misra2 required-rules
-do-not-generate-results-for all-headers
-main-generator
-results-dir C:\Polyspace\MyCodeProverProject

listofoptions.txt ファイル内のオプションを使用して Polyspace を実行します。
```
polyspace-code-prover -options-file listofoptions.txt
```

-options-file も参照してください。

ビルドシステムからのオプションファイル作成

ビルドコマンド (makefile) を使用してソースコードをビルドする場合は、ビルドコマンドからソースおよびコンパイラオプションをまとめることができます。ビルドコマンドをトレースして、必要な Polyspace オプションを含むテキストファイルを生成します。

コンフィギュレーションツールを使用して Polyspace オプションのリストを作成します。
```
polyspace-configure -output-options-file \
        myOptions buildCommand
```
ここで、buildCommand はソースコードのビルドに使用するコマンド (make -B など) です。
polyspace-configure も参照してください。
ビルドから読み取ったオプションを使用して Polyspace を実行します。
```
polyspace-bug-finder -options-file myOptions \
        -results-dir myResults
```
ビルドコマンドからまとめたオプションに加えて、欠陥チェッカーを指定するなどの目的で、さらにオプションを追加する場合があります。これらのオプションをオプションファイルに追加したり、コマンドラインで直接追加したり、別の -options-file フラグを使用して 2 番目のオプションファイルから追加したりすることができます。
Polyspace ユーザーインターフェイスで結果を開きます。
```
polyspace-bug-finder myResults
```

参考

polyspace-configure | polyspace-bug-finder | polyspace-code-prover (Polyspace Code Prover)

外部の Web サイト

Jenkins による連続的コード検証の設定