Если анализ Polyspace® вашего кода находит известные или приемлемые дефекты или кодирующий нарушения правила, можно подавить дефекты или нарушения в последующих исследованиях. Добавьте аннотации кода, указывающие, что вы рассмотрели проблемы и что вы не намереваетесь зафиксировать их.
Можно добавить аннотации через пользовательский интерфейс Polyspace или путем ввода их непосредственно в коде. Для общего рабочего процесса смотрите Результаты Polyspace Адреса Через Исправления ошибок или Выравнивания. Эта тема показывает синтаксис аннотации.
Обратите внимание на то, что вы не можете скрыть ошибки времени выполнения, обнаруженные с Программой автоматического доказательства Кода из вашего исходного кода даже с аннотациями кода. Однако как все другие результаты, информация об анализе, сопоставленная с ошибкой времени выполнения, извлечена из соответствующей аннотации кода и показана результатом.
Чтобы добавить комментарии непосредственно в ваш исходный файл, используйте синтаксис аннотации Polyspace. Синтаксис не является чувствительным к регистру, и имеет следующий формат. Оба C разрабатывают комментарии в /* */ и C++ разрабатывает комментарии начиная с // поддерживаются.
Чтобы аннотировать результат на текущей строке кода (включая макросы), используйте этот синтаксис:
line of code; /* polyspace Family:Result_name */
Аннотации начинаются с ключевого слова polyspace и должен включать Family и Result_name значения полей. Можно опционально задать Status, Severity, и Comment значения полей.
polyspace Family:Result_name [Status:Severity] "Comment"
Если вы не задаете состояние, Polyspace считает результат выровненным по ширине и присваивает состояние No action planned к результату.
Для получения дальнейшей информации смотрите Детали Синтаксиса Аннотации и Примеры Синтаксиса.
Чтобы аннотировать блок кода, используйте следующий синтаксис.
Аннотация для текущей строки кода и n следующие линии:
code; /* polyspace +n Family:Result_name */
Аннотация для блока кода:
/* polyspace-begin Family:Result_name */ code; /* polyspace-end Family:Result_name */
Опционально, задайте состояние, серьезность и комментарий.
Если аннотации для результатов с тем же Family и Result_name вкладываются, самая внутренняя аннотация используется.
Например, в этом коде, аннотация на линию 9 применяется вместо аннотации блока, но аннотация блока применяется к нарушению на линии 7.
1 /*polyspace-begin MISRA-C:14.9 [To fix:High] "Block annotation"*/ 2 int main(void) 3 { 4 int x = 1; 5 int y = x / 2; 6 7 if (y < 0) /* Block annotation is applied to this violation of MISRA-C:14.9*/ 8 y++; 9 if (x > y) /*polyspace MISRA-C:14.9 [Justified:Low] "Nested annotation applied"*/ 10 return x; 11 return x; 12 } 13 /*polyspace-end MISRA-C:14.9 [To fix:High] "Block annotation"*/ |
Для получения дальнейшей информации смотрите Детали Синтаксиса Аннотации и Примеры Синтаксиса.
Чтобы выровнять по ширине несколько результатов в той же аннотации, используйте следующий синтаксис.
Если результаты принадлежат тому же семейству, задают разделенные от запятой имена результата.
line of code; /* polyspace Family:Result_1_name,Result_2_name */
Если результаты принадлежат различным семействам, задают разделенные пробелом фамилии.
line of code; /* polyspace Family_1:Result_1_name Family_2:Result_2_name */
Опционально, задайте состояние, серьезность и комментарий.
Для получения дальнейшей информации смотрите Детали Синтаксиса Аннотации и Примеры Синтаксиса.
Чтобы заменить различные поля аннотации на их позволенные значения, используйте значения в этой таблице или смотрите примеры.
| Поле | Позволенное значение |
|---|---|
Family | Тип результата анализа:
Чтобы задать все результаты анализа, используйте символ звездочки Смотрите примеры синтаксиса. |
Result_name | Для Для Для Для Для кодирования стандартных нарушений задайте номер правила или числа. Чтобы задать все части результата называют Смотрите примеры синтаксиса. |
Status | Текст, чтобы указать, как вы намереваетесь исправить ошибку в своем коде. Это значение заполняет столбец Status в панели Results List как:
Polyspace подавляет результаты, аннотируемые состоянием |
Severity | Текст, чтобы указать, как очень важный вы рассматриваете ошибку в своем коде. Это значение заполняет столбец Severity в панели Results List как:
Если вы задаете серьезность, которая не является позволенным значением, Polyspace добавляет его к полю состояния и хранит его как пользовательское состояние. Например, |
Comment | Дополнительный текст, такой как ключевое слово или объяснение состояния и серьезности. Это значение заполняет столбец Comment в панели Results List. Дополнительный текст может охватить больше чем одну линию в коде. При показе этого текста в отчетах начальные и конечные пробелы на линии объединены в один пробел так, чтобы целый текст мог быть считан как одиночный абзац. |
Введите аннотацию на ту же линию как дефект и задайте Family (DEFECT) и Result_name (INT_OVFL). Когда вы не задаете состояние, Polyspace присваивает состояние No action planned, и затем подавляет результат в последующих исследованиях.
int var = INT_MAX; var++;/* polyspace DEFECT:INT_OVFL */ |
Выровняйте по ширине кодирующее стандартное нарушение, например, нарушение CERT-C.
Введите аннотацию на ту же линию как нарушение и задайте Family (CERT-C) и Result_name (номер правила, например, STR31-C). Присвойте состояние Justified, серьезность Low и комментарий.
code; /* polyspace CERT-C:STR31-C [Justified:Low] "Overflow cannot happen
because of external constraints." */ |
Введите аннотацию с +n между polyspace и Family:Result_name записи. Аннотация применяется к той же линии и n следующие линии.
Эта аннотация применяется к линиям 4–7. Количество линии включает код, комментарии и пустые строки.
4. code ; // polyspace +3 MISRA2012:*
5. //comment
6.
7. code;
8. code; |
Чтобы аннотировать метрики сложности кода функционального уровня, в функциональном определении, вводят аннотацию на ту же линию как имя функции.
Эта аннотация подавляет все метрики сложности кода для функционального func:
char func(char param) { //polyspace CODE-METRICS:*
...
} |
Введите каждое семейство, разделенное пробелом. Эта аннотация применяется ко всем правилам MISRA C:2012 17 и ко всем проверкам на этапе выполнения.
some code; /* polyspace MISRA2012:17.* RTE:* */ |
После того, как вы задаете Family (DEFECT), введите каждый Result_name разделенный запятой.
system("rm ~/.config"); /* polyspace DEFECT:UNSAFE_SYSTEM_CALL,RETURN_NOT_CHECKED */ |
После того, как вы задаете Family и Result_name, можно добавить Comment с дополнительной информацией для вашего выравнивания. Можно предоставить комментарий всем семействам и закончиться имена или комментарий для каждого семейства или закончиться имя.
//Single comment code; /* polyspace DEFECT:BAD_FREE MISRA2004:* "Comment applies to defect and Misra C:2004 rules" */ //Multiple comments incorrect syntax: code; /* polyspace DEFECT:* "Comment applies to all defects" MISRA2004:5.2 "Comment applies to Misra C: 2004 rule 5.2" */ //Multiple comments correct syntax: code; /* polyspace DEFECT:* "Comment applies to all defects" polyspace MISRA2004:5.2 "Comment applies to Misra C: 2004 rule 5.2" */ |
В аннотациях Polyspace игнорирует весь текст после двойных кавычек. Задавать дополнительный Family:Result_nameСостояние:Severity] или Comment записи, необходимо повторно войти в ключевое слово polyspace после текста в двойных кавычках.
Можно задать позволенные значения или ввести пользовательские значения для состояния и серьезности. Пользовательская запись серьезности добавлена к состоянию и сохранена как пользовательский Status в пользовательском интерфейсе.
//Set Status only code; /* polyspace DEFECT:* [To fix] "some comment" */ //Set Status 'To fix' and Severity 'High' code; /* polyspace VARIABLE:* [To fix: High] "some comment"*/ //Set custom status 'Assigned' and Severity 'Medium' code; /* polyspace MISRA2012:12.* [Assigned: Medium] */ |
