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 или FALSE

Когда вы устанавливаете этот атрибут на "истинный", регулярное выражение является нечувствительным к регистру, в противном случае это является чувствительным к регистру. Если вы не объявляете этот атрибут в своем выражении, регулярное выражение является чувствительным к регистру. Для 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®: 2 012 правил 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: 2 012 правил:

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

Поддержка