-xml-annotations-description

Примените аннотации пользовательского кода к результатам анализа Polyspace

Синтаксис

-xml-annotations-description file_path

Описание

-xml-annotations-description file_path использует синтаксис аннотации, заданный в XML-файле, расположенном в file_path интерпретировать аннотации кода в ваших исходных файлах. Можно использовать XML-файл, чтобы задать синтаксис аннотации и сопоставить его с синтаксисом аннотации Polyspace®. Когда вы запускаете анализ при помощи этой опции, можно выровнять по ширине и скрыть результаты с аннотациями, которые используют синтаксис. Если при запуске Polyspace в командной строке, file_path абсолютный путь или путь относительно папки, от которой вы запускаете команду. Если при запуске Polyspace через пользовательский интерфейс, file_path абсолютный путь.

Если при запуске анализ через пользовательский интерфейс, можно ввести эту опцию в поле Other под узлом Advanced Settings на панели Configuration. Смотрите Other.

Если вы используете Polyspace в качестве Вас Расширения кода в ИДАХ, введите эту опцию в файл опций анализа. Смотрите файл опций.

Почему использование эта опция

Если у вас есть существующие аннотации от предыдущих рассмотрений кода, можно импортировать эти аннотации к Polyspace. Вы не должны рассмотреть и выровнять по ширине результаты, которые вы уже аннотировали. Точно так же, если ваши комментарии к коду должны придерживаться определенного формата, можно сопоставить и импортировать тот формат к Polyspace.

Примеры

Импортируйте существующие аннотации для кодирования нарушений правила

Предположим, что вы ранее рассмотрели исходный файл zero_div.c содержа следующий код и выровненный по ширине определенный MISRA C®: 2 012 нарушений при помощи пользовательских аннотаций.

#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 в один пронумерованный список. В этом списке правила 8.4 и 8.7 соответствуют числам 50 и 51. Можно проверять этот код на MISRA C: 2 012 нарушений путем ввода команды:

  • Bug Finder:

    polyspace-bug-finder -sources source_path -misra3 all
  • Программа автоматического доказательства кода:

    polyspace-code-prover -sources source_path -misra3 all -main-generator
  • Сервер Bug Finder:

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

  • Сервер программы автоматического доказательства кода:

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

source_path путь к zero_div.c.

Аннотируемые нарушения появляются в панели Results List. Необходимо рассмотреть и выровнять по ширине их снова.

Этот пример XML задает формат аннотации, используемый в zero_div.c и карты это к синтаксису аннотации Polyspace:

  • Формат аннотации является ключевым словом My_rule, сопровождаемый пробелом и одним или несколькими разделенными от запятой алфавитно-цифровыми идентификаторами правила.

  • Постановите, что идентификаторы 50 и 51 сопоставлены с MISRA C: 2 012 правил 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-desription ^
      C:\Polyspace_workspace\annotations\annotations_description.xml
    • Программа автоматического доказательства кода:

      polyspace-code-prover -sources source_path -misra3 all ^
      -main-generator -xml-annotations-desription ^
      C:\Polyspace_workspace\annotations\annotations_description.xml
    • Сервер Bug Finder:

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

    • Сервер программы автоматического доказательства кода:

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

Polyspace считает аннотируемые результаты выровненными по ширине и скрывает их в панели Results List.

Введенный в R2017b