-xml-annotations-description

Polyspace 解析結果に対するカスタム コード注釈の適用

構文

-xml-annotations-description file_path

説明

-xml-annotations-description file_path では、file_path にある XML ファイルで定義された注釈構文を使用して、ソース ファイルのコード注釈を解釈します。この XML ファイルを使用して注釈構文を指定し、それを Polyspace® 注釈構文にマッピングできます。このオプションを使用して解析を実行する場合は、構文を使用した注釈によって結果を正当化して非表示にできます。コマンド ラインで Polyspace を実行する場合、file_path は絶対パス、またはコマンドを実行するフォルダーからの相対パスです。ユーザー インターフェイスから Polyspace を実行する場合、file_path は絶対パスです。

ユーザー インターフェイス (Polyspace デスクトップ製品のみ) では、[構成] ペインの [その他] フィールドにこのオプションを入力します。Otherを参照してください。

IDE で Polyspace as You Code の拡張機能を使用する場合は、このオプションを解析オプション ファイルに入力します。オプション ファイルを参照してください。

このオプションを使用する理由

以前のコード レビューの既存の注釈がある場合は、その注釈を Polyspace にインポートできます。既に注釈が付けられている結果は、レビューして正当化する必要はありません。同様に、コード コメントが特定の形式に従わなければならない場合、その形式を Polyspace にマッピングおよびインポートできます。

例

コーディング ルール違反に関する既存の注釈のインポート

以前に次のコードを含むソース ファイル zero_div.c をレビューし、カスタム注釈を使用して特定の MISRA C™:2012 違反を正当化したとします。

#include <stdio.h>

/* Violation of Misra C:2012 
rules 8.4 and 8.7 on the next
line of code. */

int func(int p) //My_rule 50, 51
{	
    int i;
    int j = 1;

    i = 1024 / (j - p); 
    return i;
}

/* Violation of Misra C:2012 
rule 8.4 on the next line of 
code */

int func2(void){ //My_rule 50
	int x=func(2);
	return x; 
}
コード コメント My_rule 50, 51 および My_rule 50 では、Polyspace 注釈構文を使用していません。代わりに、すべての MISRA ルールを単一の番号付きリストに配置するという規則を使用しています。このリストでは、Rule 8.4 と 8.7 が番号 50 と 51 に対応します。次のコマンドを入力することで、このコードの MISRA C:2012 違反をチェックできます。

  • Bug Finder:

    polyspace-bug-finder -sources source_path -misra3 all

  • Code Prover:

    polyspace-code-prover -sources source_path -misra3 all -main-generator

  • Bug Finder Server:

    polyspace-bug-finder-server -sources source_path -misra3 all

  • Code Prover Server:

    polyspace-code-prover-server -sources source_path -misra3 all -main-generator

source_path は zero_div.c のパスです。

注釈が付けられた違反は [結果のリスト] ペインに表示されます。それを再度レビューし、正当化しなければなりません。

この XML の例では、zero_div.c で使用する注釈形式を定義して、それを Polyspace 注釈構文にマッピングしています。

  • 注釈は、キーワード My_rule の後にスペースと 1 つ以上のコンマ区切りの英数字のルール識別子が続く形式です。

  • ルール識別子 50 と 51 は、MISRA C:2012 Rule 8.4 と 8.7 にそれぞれマッピングされています。マッピングでは Polyspace 注釈構文を使用します。 

<?xml version="1.0" encoding="UTF-8"?>

<Annotations xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
             xsi:noNamespaceSchemaLocation="annotations_xml_schema.xsd"
             Group="exampleCustomAnnotation">
			 
  <Expressions Search_For_Keywords="My_rule"
			  Separator_Result_Name="," >
			  
								
	<!-- This section defines the annotation syntax format -->		  
   <Expression Mode="SAME_LINE"
               Regex="My_rule\s(\w+(\s*,\s*\w+)*)"
               Rule_Identifier_Position="1"
               />
			   
 </Expressions>
  <!-- This section maps the user annotation to the Polyspace
  annotation syntax -->
 <Mapping>
    <Result_Name_Mapping  Rule_Identifier="50" Family="MISRA-C3" Result_Name="8.4"/>
	<Result_Name_Mapping  Rule_Identifier="51" Family="MISRA-C3" Result_Name="8.7"/>
   </Mapping>
</Annotations>

既存の注釈をインポートして対応する Polyspace 結果に適用するには、以下を行います。

  1. 前述のコード例をテキスト エディターにコピーして、annotations_description.xml という名前でマシンの C:\Polyspace_workspace\annotations\ などの場所に保存します。

  2. 次のコマンドを使用して zero_div.c の解析を再実行します。

    • Bug Finder:

      polyspace-bug-finder -sources source_path -misra3 all ^
-xml-annotations-description ^
C:\Polyspace_workspace\annotations\annotations_description.xml

    • Code Prover:

      polyspace-code-prover -sources source_path -misra3 all ^
-main-generator -xml-annotations-description ^
C:\Polyspace_workspace\annotations\annotations_description.xml

    • Bug Finder Server:

      polyspace-bug-finder-server -sources source_path -misra3 all ^
-xml-annotations-description ^
C:\Polyspace_workspace\annotations\annotations_description.xml

    • Code Prover Server:

      polyspace-code-prover-server -sources source_path -misra3 all ^
-main-generator -xml-annotations-description ^
C:\Polyspace_workspace\annotations\annotations_description.xml

Polyspace では、注釈の付けられた結果は正当化されていると見なし、[結果のリスト] ペインに表示しません。

バージョン履歴

R2017b で導入

参考

トピック