Эти подмножества инструкций MISRA® C:2012 могут оказать прямое или косвенное влияние на точность ваших результатов Polyspace®. Когда вы настраиваете проверку правил кодирования, можно выбрать эти подмножества.
SQO-Subset1Следующий набор MISRA C:2012, кодирующего инструкции обычно, сокращает количество бездоказательных результатов в Polyspace Code Prover™.
| Правило | Описание |
|---|---|
| 8.8 | Статический спецификатор класса памяти должен использоваться во всех объявлениях объектов и функций, которые имеют внутреннюю связь |
| 8.11 | Когда массив с внешней связью объявляется, ее размер должен быть явным образом задан |
| 8.13 | Указатель должен указать на квалифицированный к const тип, когда это возможно, |
| 11.1 | Преобразования не должны выполняться между указателем на функцию и любым другим типом |
| 11.2 | Преобразования не должны выполняться между указателем на неполный тип и любым другим типом |
| 11.4 | Преобразование не должно быть выполнено между указателем на объект и целочисленным типом |
| 11.5 | Преобразование не должно быть выполнено от указателя, чтобы освободить в указатель на объект |
| 11.6 | Бросок не должен выполняться между указателем на пустоту и арифметическим типом |
| 11.7 | Бросок не должен выполняться между указателем на объект и типом арифметики нецелого числа |
| 14.1 | Счетчик цикла не должен иметь чрезвычайно типа с плавающей точкой |
| 14.2 | Цикл for должен быть правильно построен |
| 15.1 | Оператор перехода не должен использоваться |
| 15.2 | Оператор перехода должен перейти к метке, объявленной позже в той же функции |
| 15.3 | Любая метка, на которую ссылается оператор перехода, должна быть объявлена в том же блоке, или в любом блоке, заключающем оператор перехода |
| 15.5 | Функция должна иметь одну точку выхода в конце |
| 17.1 | Функции <starg.h> не должны быть использованы |
| 17.2 | Функции не должны вызывать себя, ни один прямо или косвенно |
| 18.3 | Операторы отношения>,> =, <и <= не должны быть применены к объектам типа указателя кроме того, где они указывают в тот же объект |
| 18.4 | +, - + = и - = операторы не должны быть применены к выражению типа указателя |
| 18.5 | Объявления должны содержать не больше, чем два уровня вложения указателя |
| 18.6 | Адрес объекта с автоматическим хранением не должен быть скопирован в другой объект, который сохраняется после того, как первый объект прекратил существование |
| 19.2 | Ключевое слово объединения не должно использоваться |
| 21.3 | Функции выделения памяти и освобождения <stdlib.h> не должны использоваться |
SQO-Subset2Хорошие методы проекта обычно приводят к меньшему количеству сложности кода, которая может сократить количество бездоказательных результатов в Polyspace Code Prover. Следующий набор кодирования правил осуществляет хорошие методы проекта. Опция SQO-subset2 проверяет правила в SQO-subset1 и некоторые дополнительные правила.
| Правило | Описание |
|---|---|
| 8.8 | Статический спецификатор класса памяти должен использоваться во всех объявлениях объектов и функций, которые имеют внутреннюю связь |
| 8.11 | Когда массив с внешней связью объявляется, ее размер должен быть явным образом задан |
| 8.13 | Указатель должен указать на квалифицированный к const тип, когда это возможно, |
| 11.1 | Преобразования не должны выполняться между указателем на функцию и любым другим типом |
| 11.2 | Преобразования не должны выполняться между указателем на неполный тип и любым другим типом |
| 11.4 | Преобразование не должно быть выполнено между указателем на объект и целочисленным типом |
| 11.5 | Преобразование не должно быть выполнено от указателя, чтобы освободить в указатель на объект |
| 11.6 | Бросок не должен выполняться между указателем на пустоту и арифметическим типом |
| 11.7 | Бросок не должен выполняться между указателем на объект и типом арифметики нецелого числа |
| 11.8 | Бросок не должен удалять const или энергозависимую проверку от типа, на который указывает указатель |
| 12.1 | Приоритет операторов в рамках выражений должен быть сделан явным |
| 12.3 | Оператор запятой не должен использоваться |
| 13.2 | Значение выражения и его персистентных побочных эффектов должно быть тем же самым согласно всем разрешенным порядкам оценки |
| 13.4 | Результат оператора присваивания не должен использоваться |
| 14.1 | Счетчик цикла не должен иметь чрезвычайно типа с плавающей точкой |
| 14.2 | Цикл for должен быть правильно построен |
| 14.4 | Выражение управления оператора if и выражение управления оператора цикла должны иметь по существу булев тип |
| 15.1 | Оператор перехода не должен использоваться |
| 15.2 | Оператор перехода должен перейти к метке, объявленной позже в той же функции |
| 15.3 | Любая метка, на которую ссылается оператор перехода, должна быть объявлена в том же блоке, или в любом блоке, заключающем оператор перехода |
| 15.5 | Функция должна иметь одну точку выхода в конце |
| 15.6 | Тело оператора цикла или выбора - оператор должно быть составным оператором - |
| 15.7 | Все, если … еще, если построения еще должны быть отключены с оператор |
| 16.4 | Каждый оператор switch должен иметь метку по умолчанию |
| 16.5 | Метка по умолчанию должна появиться или как первое или как последняя метка переключателя оператора switch |
| 17.1 | Функции <starg.h> не должны быть использованы |
| 17.2 | Функции не должны вызывать себя, ни один прямо или косвенно |
| 17.4 | Все выходные пути от функции с непустым типом возврата должны иметь явный оператор возврата с выражением |
| 18.3 | Операторы отношения>,> =, <и <= не должны быть применены к объектам типа указателя кроме того, где они указывают в тот же объект |
| 18.4 | +, - + = и - = операторы не должны быть применены к выражению типа указателя |
| 18.5 | Объявления должны содержать не больше, чем два уровня вложения указателя |
| 18.6 | Адрес объекта с автоматическим хранением не должен быть скопирован в другой объект, который сохраняется после того, как первый объект прекратил существование |
| 19.2 | Ключевое слово объединения не должно использоваться |
| 20.4 | Макрос не должен быть задан с тем же именем как ключевое слово |
| 20.6 | Лексемы, которые похожи на директиву предварительной обработки, не должны происходить в макро-аргументе |
| 20.7 | Выражения, следующие из расширения макро-параметров, должны быть заключены в круглые скобки |
| 20.9 | Все идентификаторы, используемые в выражении управления #if или директив предварительной обработки #elif, должны быть #define'd перед оценкой |
| 20.11 | Макро-параметр сразу после # оператора не должен сразу сопровождаться ## оператором |
| 21.3 | Функции выделения памяти и освобождения <stdlib.h> не должны использоваться |