Exponenta Banner

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

Этот пример показывает, как создать и отредактировать XML-файл, чтобы задать формат аннотации и сопоставить его с синтаксисом аннотации Polyspace®.

Чтобы начать, скопируйте следующий код в текстовый редактор и сохраните его на своей машине как 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, ваш синтаксис должен следовать за шаблоном, который можно представлять с регулярным выражением. Смотрите Регулярные выражения (MATLAB). Рекомендуется, чтобы вы включали ключевое слово в шаблон вашего синтаксиса аннотации, чтобы помочь идентифицировать его. В этом примере ключевым словом является 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НеобходимыйСтрока поиска регулярного выражения

Смотрите Регулярные выражения (MATLAB). 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

Смотрите также

|

Похожие темы

Документация Polyspace Code Prover
Поддержка