polyspace-autosar

(システム コマンド) AUTOSAR ソフトウェア コンポーネントのコード実装に対する Polyspace Code Prover の実行

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

構文

polyspace-autosar -create-project projectFolder -arxml-dir arxmlFolder -sources-dir codeFolder [-sources-dir codeFolder] [OPTIONS]
polyspace-autosar -create-project projectFolder -arxml-dir arxmlFolder -sources-dir codeFolder -output-platform-project
polyspace-autosar -create-project projectFolder -select-arxml-files arxmlFiles [-select-arxml-files arxmlFiles] -select-source-files codeFiles [-select-source-files codeFiles] [OPTIONS]
polyspace-autosar -update-project prevProjectFile [OPTIONS]
polyspace-autosar -update-and-clean-project prevProjectFile [OPTIONS]
polyspace-autosar -help

説明

polyspace-autosar システム コマンドは、AUTOSAR ソフトウェア コンポーネントの C/C++ コード実装に、ランタイム エラーと、AUTOSAR XML 仕様のデータ制約違反がないかどうかをチェックします。

メモ

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

polyspace-autosar -create-project projectFolder -arxml-dir arxmlFolder -sources-dir codeFolder [-sources-dir codeFolder] [OPTIONS] は、AUTOSAR ソフトウェア コンポーネントのコード実装に、ランタイム エラーと、対応する AUTOSAR XML 仕様のデータ制約違反がないかどうかをチェックします。解析では、arxmlFolder 内の AUTOSAR XML 仕様 (.arxml ファイル) を解析し、その仕様に基づいて codeFolder 内のコード実装 (.c ファイル) をモジュール化して、チェックのために各モジュールに対して Code Prover を実行します。Code Prover の結果は projectFolder に保存されます。解析後、Polyspace ユーザー インターフェイスで projectFolder からプロジェクト psar_project.psprj を開くことができます。各ソフトウェア コンポーネントの結果を個別に確認することも、結果を Polyspace Access™ にアップロードして概要を確認することもできます。

トラブルシューティングのために追加オプションを使用して、たとえば、更新した特定部分のみを実行して問題を見つけ出したり、追加のヘッダー ファイルを指定したり、マクロを定義したりできます。

例

polyspace-autosar -create-project projectFolder -arxml-dir arxmlFolder -sources-dir codeFolder -output-platform-project は、AUTOSAR ソフトウェア コンポーネントのコード実装に、ランタイム エラーと、対応する AUTOSAR XML 仕様のデータ制約違反がないかどうかをチェックします。解析では、arxmlFolder 内の AUTOSAR XML 仕様 (.arxml ファイル) を解析し、その仕様に基づいて codeFolder 内のコード実装 (.c ファイル) をモジュール化します。ソフトウェア コンポーネントごとにプロジェクトが作成され、これらのプロジェクトがすべてワークスペース内に保存されます。解析では、チェックのために各モジュールに対して Code Prover を実行します。Code Prover の結果は projectFolder に保存されます。解析後、Polyspace Platform ユーザー インターフェイスで projectFolder からワークスペース psar_workspace.pswks を開くことができます。各ソフトウェア コンポーネントの結果を個別に確認することも、結果を Polyspace にアップロードして概要を取得することもできます。

polyspace-autosar -create-project projectFolder -select-arxml-files arxmlFiles [-select-arxml-files arxmlFiles] -select-source-files codeFiles [-select-source-files codeFiles] [OPTIONS] は、前述の構文のように AUTOSAR 仕様から Polyspace プロジェクトを作成しますが、シェル パターンや正規表現を使用して特定のファイルまたはフォルダーを除外することができます。

polyspace-autosar -update-project prevProjectFile [OPTIONS] は、前回の解析以降の ARXML ファイルまたは C ソース コードの変更に基づいて Code Prover の解析結果を更新します。この更新では、前回の解析の html ファイル prevProjectFile を使用し、前回の解析以降に変更されたソフトウェア コンポーネントのコード実装のみを再解析します。

トラブルシューティングでは追加オプションを使用できます。

例

polyspace-autosar -update-and-clean-project prevProjectFile [OPTIONS] は、前回の解析以降の ARXML ファイルまたは C ソース コードの変更に基づいて Code Prover の解析結果を更新します。この更新では、前回の解析以降に変更されたソフトウェア コンポーネントのコード実装のみを再解析します。クリーンな更新では無効なソフトウェア コンポーネントに関する情報の削除も行います。たとえば、特定のソフトウェア コンポーネントの更新を強制する追加オプションを使用していて、他のソフトウェア コンポーネントも変更されている場合、クリーンな更新ではこれらの他のソフトウェア コンポーネントを Polyspace プロジェクトから削除します。

トラブルシューティングでは追加オプションを使用できます。

例

polyspace-autosar -help は、polyspace-autosar で利用できるすべてのオプションを表示します。

例

すべて折りたたむ

現在のフォルダーに含まれる arxml フォルダーに ARXML ファイルがあり、code フォルダーに C ソース ファイルがあるとします。

ARXML ファイルで定義されたすべてのソフトウェア コンポーネントに対して Code Prover を実行します。結果を現在のフォルダー内にあるフォルダー polyspace に保存します。

polyspace-autosar -create-project polyspace -arxml-dir arxml -sources-dir code

解析では、複数のモジュールを使用して Polyspace プロジェクトを作成します。各モジュールはソフトウェア コンポーネントの C コード実装をまとめます。解析では、各モジュールに対して Code Prover を実行し、コードにランタイム エラーまたは ARXML 仕様の不一致がないかどうかをチェックします。

解析後、いくつかの方法で結果を開くことができます。AUTOSAR コードに対する Polyspace の結果のレビューを参照してください。

ARXML またはコード ファイルを更新します。たとえば、Linux® では、ファイルに touch コマンドを実行して、更新を示すことができます。Code Prover 解析の結果が更新による影響を受けたかどうかをチェックします。更新された解析を得るには、前の手順で作成したプロジェクト ファイル psar_project.html を指定します。

polyspace-autosar -update-project polyspace\psar_project.xhtml

ARXML ファイルを更新した場合、解析全体が繰り返されます。ソース コードを更新した場合、更新されたコード実装のあるソフトウェア コンポーネントに対してのみ、解析が繰り返されます。

すべてのソフトウェア コンポーネントに対して Code Prover を実行する代わりに、特定のソフトウェア コンポーネントのみをチェックします。

たとえば、ソフトウェア コンポーネントに完全修飾パス pkg.component.bhv があるとします。このソフトウェア コンポーネントのみに対して Code Prover を実行できます。

polyspace-autosar -create-project polyspace -arxml-dir arxml -sources-dir code -autosar-behavior pkg.component.bhv

すべてのソフトウェア コンポーネントに対して Code Prover を実行して、後で特定のソフトウェア コンポーネントについてのみ解析を更新するように選択できます。

polyspace-autosar -update-project polyspace\psar_project.xhtml -autosar-behavior pkg.component.bhv

更新されたソフトウェア コンポーネントを再解析していなければ、解析では、そのソフトウェア コンポーネントが無効になっている可能性があると示されます。

特定のソフトウェア コンポーネントの解析を更新して、他のソフトウェア コンポーネントのすべてのトレースを削除することもできます。

polyspace-autosar -update-and-clean-project polyspace\psar_project.xhtml -autosar-behavior pkg.component.bhv

入力引数

すべて折りたたむ

フォルダー名。(二重引用符で囲んで) 文字列として指定します。このフォルダーが存在する場合、フォルダーは空でなければなりません。

解析後、このフォルダーには 2 つのプロジェクト ファイル psar_project.psprj および psar_project.html が含まれます。

  • 結果を確認するには、ファイル psar_project.psprj を Polyspace ユーザー インターフェイスで開くか、ファイル psar_project.html を Web ブラウザーで開きます。

  • 以降の更新については、コマンド ラインでファイル psar_project.html を使用します。

AUTOSAR コードに対する Polyspace の結果のレビューも参照してください。

例: "C:\Polyspace_Projects\proj_swc1"

フォルダー名。(二重引用符で囲んで) 文字列として指定します。フォルダー パスにスペースが含まれていない場合は二重引用符を省略できます。

フォルダー名の UNC パスはサポートされていません。

例: "C:\arxml_swc1"

フォルダー名。(二重引用符で囲んで) 文字列として指定します。フォルダー パスにスペースが含まれていない場合は二重引用符を省略できます。

ソースを含む複数のルート フォルダーを指定するには、-sources-dir オプションを繰り返します。複数のルート フォルダーを指定する場合、ルート フォルダーが重複してはなりません。たとえば、ルート フォルダーを別のルート フォルダーのサブフォルダーにすることはできません。

フォルダー名の UNC パスはサポートされていません。

例: "C:\code_swc1"

ARXML ファイルの後ろに、文字列として指定されたファイルとフォルダーの包含と除外が続くルート フォルダー。この文字列を作成するには、次のようにします。

  1. Linux find コマンドを使用して、包含または除外するファイルとフォルダーを検索します。

  2. find オプションをコピーして、それらを二重引用符で囲みます。

例については、Polyspace 解析用の AUTOSAR XML (ARXML) ファイルとコード ファイルの選択を参照してください。

コード (.c と .h) ファイルの後ろに、文字列として指定されたファイルとフォルダーの包含と除外が続くルート フォルダー。この文字列を作成するには、次のようにします。

  1. Linux find コマンドを使用して、包含または除外するファイルとフォルダーを検索します。

  2. find オプションをコピーして、それらを二重引用符で囲みます。

例については、Polyspace 解析用の AUTOSAR XML (ARXML) ファイルとコード ファイルの選択を参照してください。

前に作成したプロジェクト ファイル psar_project.html へのパスです。(二重引用符で囲んで) 文字列として指定します。フォルダー パスにスペースが含まれていない場合は二重引用符を省略できます。

例: "C:\Polyspace_Projects\proj1\psar_project.html"

Polyspace プロジェクトの作成および以降の解析を制御するためのオプションです。主にこのオプションはトラブルシューティングで使用し、たとえば、更新した特定部分のみを実行して問題を絞り込んだり、追加のヘッダー ファイルを指定したり、マクロを定義したりします。

一般的なオプション

オプション説明
-verbose

コマンド実行のさまざまな段階に関する追加情報を保存します (詳細モード)。ファイル psar_project.log およびその他の補助ファイルにこの追加情報を保存します。

コマンド実行でエラーが発生した場合は、詳細モードを有効にしているかどうかにかかわらず、個別のファイルにエラー メッセージが保存されます。詳細モードで実行すると、実行のさまざまな段階のみが保存されます。この情報を使用することで、いつエラーが発生したのかを確認できます。

-options-file OPTION_FILE

コマンド ライン オプションを補ったり置き換えたりするにはオプション ファイルを使用します。オプション ファイルでは、個別の行で各オプションを指定します。コメントを示すには、行の先頭に # を使用します。

オプション ファイル opts.txt は以下のようになります。

# Store Polyspace results
-create-project polyspace
# ARXML Folder
-arxml-dir arxml
# SOURCE Folder
-sources-dir code

次のように polyspace-autosar を実行できます。

polyspace-autosar -options-file opts.txt

polyspace-autosar コマンドで直接指定したオプションが、オプション ファイルのオプションと競合する場合は、直接指定したオプションが使用されます。たとえば、この例では Polyspace プロジェクトの保存にフォルダー proj が使用されます。

polyspace-autosar -create-project proj -options-file opts.txt

通常、複数のプロジェクトに共通のオプションを格納したり、再利用したりするには、オプション ファイルを使用します。

-generate-autosar-headers

ソース フォルダーで見つかったヘッダーを使用する代わりに、AUTOSAR ヘッダー (Rte_ ヘッダー、および Os.h、Compiler.h など) を生成します。

プロジェクトの更新を制御するオプション

プロジェクトを更新する場合、既定では、ARXML ファイルまたは C ソース コードに対して前回の解析以降に加えられた変更について、すべての AUTOSAR ソフトウェア コンポーネントの動作に関する解析結果が更新されます。これらのオプションにより、更新を制御できるようになります。

オプション説明
-autosar-behavior AUTOSAR_QUALIFIED_NAME

AUTOSAR_QUALIFIED_NAME で指定した内部動作が備わったソフトウェア コンポーネントの実装をチェックします。既定の解析では、ARXML 仕様内に存在するすべてのソフトウェア コンポーネントが考慮されます。

複数のソフトウェア コンポーネントを指定するには、このオプションを繰り返します。または、次のいずれかを行います。

  • -select-arxml-files と -select-source-files で使用されるパターンと同様のシェル パターンを使用します。

    例については、Polyspace 解析用の AUTOSAR XML (ARXML) ファイルとコード ファイルの選択を参照してください。

  • 正規表現を使用して、同じパッケージ内にあるソフトウェア コンポーネントのグループを指定します。

    次に例を示します。

    • 完全修飾名 pkg.component.bhv をもつ内部動作が備わったソフトウェア コンポーネントを指定するには、以下を使用します。

      -autosar-behavior pkg.component.bhv

    • pkg.component で始まる完全修飾名をもつ内部動作が備わったソフトウェア コンポーネントを指定するには、以下を使用します。

      -autosar-behavior pkg.component\..*
      \. は、パッケージ名の区切り . (ドット) を表し、.* は任意の数の文字を表します。

-do-not-update-autosar-prove-environment

ARXML 仕様を読み取りません。前回の解析で保存された ARXML 仕様を使用します。

コードを以前の仕様と比較するには、プロジェクトの更新中にこのオプションを使用します。このオプションを使用しないと、プロジェクトの更新では全体の ARXML 仕様が再度読み取られます。

-do-not-update-extract-code

C ソース コードを読み取りません。前回の解析で保存されたソース コードを使用します。

前回のソース コードを ARXML の仕様と比較するには、プロジェクトの更新中にこのオプションを使用します。このオプションを使用しないと、プロジェクトの更新では前回の解析以降にソース コードに加えられたすべての変更が考慮されます。

-do-not-update-verification

ARXML 仕様と C コード実装の読み取りのみを行い、Code Prover 解析は実行しません。

ARXML 仕様に生じたエラーまたはソース コードに生じたコンパイル エラーを調査するには、プロジェクトの更新中にこのオプションを使用します。まず、これらの問題を修正してから、Code Prover 解析を実行することができます。

ARXML 仕様の解析を制御するオプション

オプション説明
-autosar-datatype AUTOSAR_QUALIFIED_NAME

AUTOSAR_QUALIFIED_NAME で指定された AUTOSAR データ型の定義をインポートします。既定の解析では、検証するソフトウェア コンポーネントの内部動作で指定されたデータ型のみがインポートされます。

複数のデータ型を指定するには、このオプションを繰り返します。または、次のいずれかを行います。

  • -select-arxml-files と -select-source-files で使用されるパターンと同様のシェル パターンを使用します。

    例については、Polyspace 解析用の AUTOSAR XML (ARXML) ファイルとコード ファイルの選択を参照してください。

  • 正規表現を使用して、同じパッケージ内にあるすべてのデータ型を指定します。

    次に例を示します。

    • 完全修飾名 pkg.datatypes.type をもつデータ型を指定するには、以下を使用します。

      -autosar-datatype pkg.datatypes.type

    • pkg.datatypes で始まる完全修飾名をもつデータ型を指定するには、以下を使用します。

      -autosar-datatype pkg.datatypes\..*
      \. は、パッケージ名の区切り . (ドット) を表し、.* は任意の数の文字を表します。

    • すべてのデータ型のインポートを強制するには、以下を使用します。

      -autosar-datatype .*\..*

-Eautosar-xmlReaderSameUuidForDifferentElements

-Eno-autosar-xmlReaderSameUuidForDifferentElements

ARXML 仕様における複数の要素に同じ汎用一意識別子 (UUID) がある場合、警告とエラーを切り替えるにはこれらのオプションを使用します。

問題が発生した場合、既定の解析はエラーで停止します。警告に変換するには、-Eno-autosar-xmlReaderSameUuidForDifferentElements を使用します。競合する UUID について、解析では最後に読み取った要素を格納し、警告を続行します。

以降の実行は引き続き警告モードを使用します。エラーに戻すには、-Eautosar-xmlReaderSameUuidForDifferentElements を使用します。

-Eautosar-xmlReaderTooManyUuids

-Eno-autosar-xmlReaderTooManyUuids

ARXML 仕様における同じ要素に異なる汎用一意識別子 (UUID) がある場合、警告とエラーを切り替えるにはこれらのオプションを使用します。

問題が発生した場合、既定の解析はエラーで停止します。警告に変換するには、-Eno-autosar-xmlReaderTooManyUuids を使用します。競合する UUID について、解析では最後に読み取った要素を格納し、警告を続行します。

以降の実行は引き続き警告モードを使用します。エラーに戻すには、オプション -Eautosar-xmlReaderTooManyUuids を使用します。

-Wno-autosar-xmlDuplicateType

このオプションを使用して、ARXML での重複する型に関する警告を非表示にします。

重複する型の警告メッセージは以下のようになります。

Type arrayType is already defined in another file.

C ソース コードの読み取りを制御するオプション

オプション説明
-include PREINCLUDE_FILE

解析に関係する各ファイルによって #include でインクルードされる、ヘッダー ファイルを指定します。たとえば、-include file1.h では、すべてのソース ファイルに行 #include 'file1.h' があるかのように解析が行われます。#include でインクルードされるファイルには、コンパイル エラーに対する Polyspace 固有の回避方法 (データ型やマクロの定義など) を含めることができます。

ファイル名だけを指定する場合、そのファイルは、コマンドが実行されるフォルダー内に存在している必要があります。他のフォルダーにあるファイルを指定するには、絶対パスまたは現在のフォルダーからの相対パスを指定します。

データ型とマクロの定義を含むヘッダー ファイルを指定できるのは、プロジェクトの作成中のみです。以降の更新では、このファイルの内容は変更できますが、新しいファイルは提供できません。ファイルの内容を変更する場合は、コード抽出と、それ以降の解析を再実行する必要があります。

複数のファイルを指定するには、ファイルごとに 1 つのオプションを入力します。たとえば、-include file1.h -include file2.h とします。

オプション -D または -U を使用して追加でマクロを定義したり、その定義を解除したりする場合、PREINCLUDE_FILE の定義と競合する定義については -D または -U の指定が優先されます。

-I INCLUDE_FOLDER

ヘッダー ファイルを含むフォルダーを指定します。解析では、このフォルダー内にある #include されたファイルを調べます。このフォルダーは、ソース コード フォルダーのサブフォルダーでなければなりません。

複数のフォルダーに対してこのオプションを繰り返します。解析では、指定した順にこれらのフォルダー内のヘッダー ファイルを調べます。

ソース コード フォルダーに含まれていないフォルダーを指定する場合は、次のオプションを使用します。

-extra-project-options "-I INCLUDE_FOLDER"

-D DEFINE

解析で定義済みと見なされなければならないマクロを指定します。

たとえば、以下を指定するとします。

-D _WIN32
その場合、プリプロセッサの条件 #ifdef _WIN32 が成功し、対応する分岐が実行されます。

-U UNDEFINE

解析で未定義と見なされなければならないマクロを指定します。

たとえば、以下を指定するとします。

-U _WIN32
その場合、プリプロセッサの条件 #ifndef _WIN32 が成功し、対応する分岐が実行されます。

Code Prover チェックを制御するオプション

オプション説明
-extra-project-options POLYSPACE_OPTIONS

Code Prover 解析の追加オプションを指定します。指定したオプションは、ARXML 解析とコード抽出には適用されず、以降の Code Prover 解析にのみ適用されます。

この方法を使用して、polyspace-code-prover または polyspace-code-prover-server コマンドで使用する解析オプションを指定します。すべての Polyspace Code Prover 解析オプションのリストを参照してください。

次に例を示します。

  • コンパイラとターゲット アーキテクチャの指定が必要な場合があります。既定では、AUTOSAR 仕様から作成されるプロジェクトのコンパイルでは、gnu4.7 コンパイラと i386 アーキテクチャを使用します。

    visual11.0 コンパイラと x86_64 アーキテクチャを指定するには、次のオプションを入力します。

    -extra-project-options "-compiler visual11.0 -target x86_64"
    コンパイラ (-compiler) および ターゲット プロセッサ タイプ (-target) も参照してください。

polyspace-code-prover の以下のオプションは指定する必要がないことに注意してください。

  • -sources: polyspace-autosar により必要なソース ファイルが抽出されます。

  • -I:polyspace-autosar の -I オプションを使用してインクルード フォルダーを指定します。

  • -data-range-specifications などの入力およびスタブオプション: ARXML ファイルの外部データ制約は、polyspace-autosar で自動的に抽出されます。制約を明示的に指定することはできません。

  • -entry-points などのマルチタスキングオプション: polyspace-autosar ではマルチタスキング解析を実行できません。データ レースを検出するには、アプリケーション全体用に個別のプロジェクトを作成し、ソース フォルダーを明示的に追加します。マルチタスキングに関連する ARXML ファイルを指定して Bug Finder を実行します。詳細は、ARXML ファイルの選択 (-autosar-multitasking) を参照してください。

  • main 生成に関連付けられているCode Prover 検証オプション: AUTOSAR の記述から Polyspace プロジェクトを作成すると、main 関数が (psar_prove_main.c ファイルに) 生成されます。main 関数で、ソフトウェア コンポーネントにランナブル エンティティを実装する関数を呼び出します。Code Prover 解析には、この生成された main が必要です。この main 関数のプロパティは変更できません。

-extra-options-file OPTIONS_FILE

オプション ファイルで Code Prover 解析の追加オプションを指定します。指定したオプションは、ARXML 解析とコード抽出には適用されず、以降の Code Prover 解析にのみ適用されます。

たとえば、ビルド コマンドをトレースして、コンパイラ オプション、マクロ定義、およびインクルード フォルダーへのパスを収集し、これらの情報を AUTOSAR ソフトウェア コンポーネントのコード実装解析のためのオプション ファイルに指定できます。

  1. 関数 polyspace-configure を使用してビルド コマンド (make など) をトレースし、以降の Code Prover 解析のためのオプション ファイルを生成します。-no-sources オプションを使用して、オプション ファイルのソースのインクルードを抑制します。

    polyspace-configure -output-options-file options.txt -no-sources make

  2. polyspace-autosar を使用して AUTOSAR コードに Code Prover を実行します。ARXML フォルダー、ソース フォルダー、およびその他のオプションを指定します。さらに、-extra-options-file オプションを使用して、先ほど生成したオプション ファイルを指定します。

    polyspace-autosar ... -extra-options-file options.txt

ビルド コマンドを使用した AUTOSAR コードに対する Polyspace の実行も参照してください。

-show-prove AUTOSAR_QUALIFIED_NAME

解析後に、AUTOSAR_QUALIFIED_NAME で指定された内部動作が備わった特定のソフトウェア コンポーネントの結果を開きます。

バージョン履歴

R2018a で導入

参考

| | |

トピック