Примените аннотации пользовательского кода к результатам анализа Polyspace
-xml-annotations-description file_path
-xml-annotations-description использует синтаксис аннотации, заданный в XML-файле, расположенном в file_pathfile_path, чтобы интерпретировать аннотации кода в ваших исходных файлах. Можно использовать XML-файл, чтобы задать синтаксис аннотации и сопоставить его с синтаксисом аннотации Polyspace®. Когда вы запускаете анализ при помощи этой опции, можно выровнять по ширине и скрыть результаты с аннотациями, которые используют синтаксис. Если при запуске Polyspace в командной строке, file_path является абсолютным путем или путем относительно папки, от которой вы запускаете команду. Если при запуске Polyspace через пользовательский интерфейс, file_path является абсолютным путем.
Если при запуске анализ через пользовательский интерфейс, можно ввести эту опцию в поле Other под узлом Advanced Settings на панели Configuration. Смотрите Other.
Если у вас есть существующие аннотации от предыдущих рассмотрений кода, можно импортировать эти аннотации к 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 main(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 нарушений путем ввода команды:
Средство поиска ошибки:
polyspace-bug-finder -sources source_path -misra3 all
Программа автоматического доказательства кода:
polyspace-code-prover -sources source_path -misra3 all
Сервер средства поиска ошибки:
polyspace-bug-finder-server -sources source_path -misra3 all
Сервер программы автоматического доказательства кода:
polyspace-code-prover-server -sources source_path -misra3 all
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="example annotation">
<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:
Скопируйте предыдущий пример кода в текстовый редактор и сохраните его на вашей машине как annotations_description.xml, например, в C:\Polyspace_workspace\annotations\.
Повторно выполните анализ zero_div.c при помощи команды:
Средство поиска ошибки:
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 ^ -xml-annotations-desription ^ C:\Polyspace_workspace\annotations\annotations_description.xml
Сервер средства поиска ошибки:
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 ^ -xml-annotations-desription ^ C:\Polyspace_workspace\annotations\annotations_description.xml
Polyspace считает аннотируемые результаты выровненными по ширине и скрывает их в панели Results List.
