Если Polyspace® анализ вашего кода находит известные или приемлемые дефекты или нарушения правил кодирования, можно подавить дефекты или нарушения в последующих анализах. Добавьте аннотации кода, указывающие, что вы просмотрели проблемы и не хотите их устранять.
Можно добавить аннотации через пользовательский интерфейс Polyspace или путем ввода их непосредственно в код. Для получения общего рабочего процесса смотрите Адрес Polyspace Результаты через исправления ошибок или обоснования. В этом разделе показан синтаксис аннотации.
Обратите внимание, что вы не можете скрыть ошибки времени выполнения, обнаруженные с помощью Code Prover, от вашего исходного кода даже с аннотациями кода. Однако, как и все другие результаты, информация проверки, связанная с ошибкой времени выполнения, извлекается из соответствующей аннотации кода и показывается с результатом.
Чтобы добавить комментарии непосредственно к исходному файлу, используйте синтаксис аннотации 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:*
...
} |
Введите каждое семейство, разделенное пространством. Эта аннотация применяется ко всем правилам 17 C:2012 MISRA и ко всем проверкам во время выполнения.
some code; /* polyspace MISRA2012:17.* RTE:* */ |
После того, как вы задаете Family (DEFECT), вводите каждое Result_name разделяется запятыми.
system("rm ~/.config"); /* polyspace DEFECT:UNSAFE_SYSTEM_CALL,RETURN_NOT_CHECKED */ |
После того, как вы задаете Family и a 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, [Status: 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] */ |
