Exponenta Banner

Задайте пользовательский формат аннотации

В этом примере показов, как создать и изменить XML- файл, чтобы задать формат аннотации и сопоставить его с Polyspace® синтаксис аннотации. После создания и редактирования XML-файла передайте файл в Polyspace с помощью опции -xml-annotations-description.

Для определения нескольких пользовательских форматов аннотаций см. раздел «Определение нескольких пользовательских синтаксисов аннотаций».

Чтобы начать, скопируйте следующий код в текстовый редактор и сохраните его на своей машине как annotations_description.xml.

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

<Annotations xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
             xsi:noNamespaceSchemaLocation="annotations_xml_schema.xsd"
             Group="example XML">
			 
	
 <Expressions Search_For_Keywords="myKeyword"
			  Separator_Result_Name="," >
    <!-- Define annotation format in this
	section by adding <Expression/> elements -->
   
   <Expression Mode="SAME_LINE"
               Regex="myKeyword\s+(\w+(\s*,\s*\w+)*)"
               Rule_Identifier_Position="1"
               />	
	
   <Expression Mode="GOTO_INCREMENT"
               Regex="myKeyword\s+(\+\d+\s)(\w+(\s*,\s*\w+)*)"
               Increment_Position="1"
		  Rule_Identifier_Position="2"     
			   />	
	
  <Expression Mode="BEGIN"
               Regex="myKeyword\s*(\w+(\s*,\s*\w+)*)\s*Block_on"
               Rule_Identifier_Position="1"
		  Case_Insensitive="true"
			   />

   <Expression Mode="END"
               Regex="myKeyword\s*(\w+(\s*,\s*\w+)*)\s*Block_off"
               Rule_Identifier_Position="1"
			   />	
   <Expression Mode="END_ALL"
               Regex="myKeyword\sBlock_off_all"
			   />
	
			
   <Expression Mode="SAME_LINE"
               Regex="myKeywords\s+(\w+(\s*,\s*\w+)*)(\s*\[(\w+\s*)*([:]\s*(\w+\s*)+)*\])*(\s*-*\s*)*([^-]*)(\s*-*)*"
               Rule_Identifier_Position="1"
	         Status_Position="4"
		  Severity_Position="6"
		  Comment_Position="8"

               />	
		
	<!-- SAME_LINE example with more complex regular expression.
		Matches the following annotations:
		//myKeywords 50 [my_status:my_severity] -Additional comment-
		//myKeywords 50 [my_status]
		//myKeywords 50 [:my_severity]
		//myKeywords 50 -Additional comment-
			-->
					
 </Expressions>
 
 <Mapping>
	<!-- Map your annotation syntax to the Polyspace annotation
	syntax by adding <Result_Name_Mapping /> elements in this section -->
    
	<Result_Name_Mapping Rule_Identifier="100" Family="RTE" Result_Name="ZDV"/>
	<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"/>
	<Result_Name_Mapping Rule_Identifier="ALL_MISRA" Family="MISRA-C3" Result_Name="*"/>

 </Mapping>
</Annotations>

XML- файл состоит из двух частей:

  • <Expressions>...</Expressions> где задается формат синтаксиса аннотации.

  • <Mapping>...</Mapping> где вы сопоставляете синтаксис с синтаксисом аннотации Polyspace.

После редактирования этого файла Polyspace может интерпретировать аннотацию пользовательского кода, когда вы вызываете опцию -xml-annotations-description.

Задайте синтаксический формат аннотации

Чтобы определить синтаксис аннотации в Polyspace, ваш синтаксис должен следовать шаблону, который можно представлять с регулярным выражением. См. раздел Регулярные выражения. Рекомендуется включить ключевое слово в шаблон синтаксиса аннотации, чтобы помочь идентифицировать его. В этом примере ключевое слово myKeyword. Установите атрибут Search_For_Keywords равен этому ключевому слову.

Как только вы знаете шаблон вашей аннотации, можно задать его в XML-файле, добавив <Expression/> элемент и определение, по крайней мере, атрибутов Mode, Regex, и Rule_Identifier_Position. Например, первый <Expression/> элемент в annotations_description.xml задает аннотацию с этими атрибутами:

  • Mode="SAME_LINE". Аннотация применяется к коду в той же линии.

  • Regex="myKeyword\s+(\w+(\s*,\s*\w+)*)". Polyspace использует регулярное выражение для поиска строки, которая начинается с myKeyword, за которым следует пространство \s+. Затем Polyspace ищет группу захвата (\w+(\s*,\s*\w+)*) который включает алфавитно-цифровой идентификатор правила \w+ и, опционально, дополнительные идентификаторы правил, разделенных запятыми (\s*,\s*\w+)*.

  • Rule_Identifier_Position="1". Целое значение этого атрибута соответствует количеству открывающих круглых скобок, предшествующих соответствующей группе захвата в регулярном выражении. В myKeyword\s+(\w+(\s*,\s*\w+)*), одна открывающая круглая скобка предшествует группе захвата идентификатора правила (\w+(\s*,\s*\w+)*). Если вы хотите соответствовать идентификаторам правил, захваченным (\s*,\s*\w+), затем вы задаете Rule_Identifier_Position="2" потому что две открывающие круглые скобки предшествуют этой группе захвата.

Список атрибутов и их значений перечислены в этой таблице. Столбец примера ссылается на формат, заданный в annotations_description.xml.

ПризнакИспользоватьЗначениеПример
ModeНеобходимыйSAME_LINE

Применяется только к той же линии, что и аннотация.

code; //myKeyword 100
GOTO_INCREMENT

Применяется к той же линии, что и аннотация, и к следующим n линиям:

3. code; // myKeyword +3 ALL_MISRA
4. /*comments */			
5.	
6. code; 
7. code;

Предыдущая аннотация применяется только к линиям 3-6.

BEGIN

Применяется к тому же линия и ко всем следующим линиям до соответствующего выражения с атрибутом Mode="END" или "END_ALL"или до конца файла.

 //myKeyword 50, 51 Block_on
 Code block 1;
 ...
END

Останавливает применение идентификатора правила, объявленного соответствующим выражением с атрибутом Mode="BEGIN".

 //myKeyword 50, 51 Block_on
 Code block 1;
 ...
 More code;
 //myKeyword 50 Block_off

Отключается только идентификатор правила 50. Идентификатор правила 51 все еще применяется.

END_ALL

Останавливает все идентификаторы правил, объявленные выражением с атрибутом Mode="BEGIN".

 //myKeyword 50, 51 Block_on
 Code block 1;
 ...
 More code;
 //myKeyword Block_off_all

Идентификаторы правил 50 и 51 отключены.

RegexНеобходимыйСтрока поиска регулярного выражения

См. раздел Регулярные выражения. Regex="myKeyword\s+(\w+(\s*,\s*\w+)*)" соответствует этим выражениям:

// myKeyword 50, 51
/* myKeyword ALL_MISRA, 100 */
Rule_Identifier_PositionОбязательно, кроме тех случаев, когда вы настраиваете Mode="END_ALL"Целое число

Целое значение этого атрибута соответствует количеству открывающих круглых скобок в регулярном выражении перед соответствующим поисковым выражением.

<Expression Mode="GOTO_INCREMENT"
            Regex="myKeyword\s+(\+\d+\s)(\w+(\s*,\s*\w+)*)"
            Increment_Position="1"
	     Rule_Identifier_Position="2"/>

Поисковое выражение идентификатора правила \w+(\s*,\s*\w+)* - после второй открывающей круглой скобки правильного выражения.

Increment_PositionТребуется только при установке Mode="GOTO_INCREMENT"Целое число

Целое значение этого атрибута соответствует количеству открывающих круглых скобок в регулярном выражении перед соответствующим поисковым выражением.

<Expression Mode="GOTO_INCREMENT"
            Regex="myKeyword\s+(\+\d+\s)(\w+(\s*,\s*\w+)*)"
            Increment_Position="1"
	     Rule_Identifier_Position="2"/>

Поисковое выражение шага \+\d+\s - после первой открывающей круглой скобки правильного выражения.

Status_Position ДополнительныйЦелое числоСм. Increment_Position пример. При использовании этого атрибута запись в аннотации отображается в столбце Status на панели Results List пользовательского интерфейса.
Severity_Position ДополнительныйЦелое числоСм. Increment_Position пример. При использовании этого атрибута запись в аннотации отображается в столбце Severity на панели Results List пользовательского интерфейса.
Comment_Position ДополнительныйЦелое числоСм. Increment_Position пример. При использовании этого атрибута запись в аннотации отображается в столбце Comment на панели Results List пользовательского интерфейса. Ваш комментарий добавляется к строке Justified by annotation in source:
Case_Insensitive ДополнительныйПравда или ложь

Когда вы устанавливаете этот атрибут в «true», регулярное выражение нечувствительно к регистру, в противном случае оно чувствительно к регистру. Если вы не объявляете этот атрибут в своем выражении, регулярное выражение чувствительно к регистру. Для Case_Insensitive="true", эти аннотации эквивалентны:

//MYKEYWORD ALL_MISRA BLOCK_ON

//mykeyword all_misra block_on

Сопоставьте вашу аннотацию с синтаксисом аннотации Polyspace

После определения формата аннотации можно сопоставить идентификаторы правил, которые вы используете, с соответствующим синтаксисом аннотации Polyspace. Вы можете сделать это отображение, добавив <Result_Name_Mapping/> элемент и определяющие атрибуты Rule_Identifier, Family, и Result_Name. Например, если идентификатор 50 правила соответствует MISRA C®: 2012 правило 8.4, сопоставить его с синтаксисом Polyspace MISRA-C3:8.4 при помощи этого элемента:

<Result_Name_Mapping Rule_Identifier="50" Family="MISRA-C3" Result_Name="8.4"/>

Список атрибутов и их значений перечислены в этой таблице. Столбец примера ссылается на формат, заданный в annotations_description.xml.

ПризнакИспользоватьЗначениеПример
Rule_IdentifierНеобходимыйОпределено пользователем. Каждое значение должно быть уникальным.Смотрите раздел отображения annotations_description.xml
FamilyНеобходимыйСоответствует семейству результатов Polyspace. Список допустимых значений см. в разделе «Допустимые значения».Смотрите раздел отображения annotations_description.xml
Result_NameНеобходимыйСоответствует именам результатов Polyspace. Список допустимых значений см. в разделе «Допустимые значения».Смотрите раздел отображения annotations_description.xml

Задайте несколько пользовательских синтаксисов аннотаций

Чтобы задать более одного синтаксиса аннотации, в XML- файлом укажите разделенный запятыми список ключевых слов, сопоставленных с каждым синтаксисом Search_For_Keywords атрибут.

Для примера, если вы используете пользовательские аннотации, следующие этим шаблонам, чтобы аннотировать нарушения правил MISRA C: 2012:

int func(int p) //customSyntax M123 $ customSyntax M124
{	
    int i;
    int j = 1;

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

int func2(void){ //otherCustomSyntax 50
	int x=func(2);
	return x; 
}
Введите следующее в XML- файл, где вы задаете пользовательский синтаксис аннотации.
<?xml version="1.0" encoding="UTF-8"?>

<Annotations xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
             xsi:noNamespaceSchemaLocation="annotations_xml_schema.xsd"
             Group="multipleCustomSyntax">
	<!-- Enter comma separated list of keywords -->		 
  <Expressions Search_For_Keywords="customSyntax,otherCustomSyntax"
			  Separator_Result_Name="$" >
			 							
	<!-- This section defines the annotation syntax format -->	  
   <Expression Mode="SAME_LINE"
               Regex="customSyntax\s(\w+(\s*,\s*\w+)*)"
               Rule_Identifier_Position="1"
               />
	<Expression Mode="SAME_LINE"
               Regex="otherCustomSyntax\s(\w+(\s*,\s*\w+)*)"
               Rule_Identifier_Position="1"
               />		   
 </Expressions>
  <!-- This section maps the user annotation to the Polyspace
  annotation syntax -->
 <Mapping>
	<!-- Mapping for customSyntax rules -->
	<Result_Name_Mapping  Rule_Identifier="M123" Family="MISRA-C3" Result_Name="8.7"/>
       <Result_Name_Mapping  Rule_Identifier="M124" Family="MISRA-C3" Result_Name="D4.6"/>
	<!-- Mapping for otherCustomSyntax rules  -->
    <Result_Name_Mapping  Rule_Identifier="50" Family="MISRA-C3" Result_Name="8.4"/>
 </Mapping>
</Annotations>
При использовании нескольких пользовательских аннотаций каждый идентификатор правила должен быть уникальным. Например, в предыдущем примере вы не можете повторно использовать идентификатор правила M123 с otherCustomSyntax.

См. также

Похожие темы

Документация Polyspace Code Prover

Поддержка