Эти подмножества MISRA® C:2012 руководства могут оказать прямое или косвенное влияние на точность вашего Polyspace® результаты. При настройке проверки правил кодирования можно выбрать эти подмножества.
SQO-Subset1Следующий набор руководств по кодированию C:2012 MISRA обычно уменьшает количество недоказанных результатов в 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 | A для цикла должна быть хорошо сформирована |
| 15.1 | Оператор goto не должен использоваться |
| 15.2 | Оператор goto должен перейти к метке, объявленной позже в той же функции |
| 15.3 | Любая метка, на которую ссылается оператор goto, должна быть объявлена в том же блоке или в любом блоке, содержащем оператор goto |
| 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. Следующий набор правил кодирования обеспечивает применение передовых методов проекта. The 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 | Приведение не должно удалять какую-либо несовпадающую или летучую проверку из типа, на который указывает указатель |
| 12.1 | Приоритет операторов в выражениях должен быть сделан явным |
| 12.3 | Оператор запятыми не должен использоваться |
| 13.2 | Значение выражения и его стойких побочных эффектов должно быть одинаковым при всех разрешенных порядках |
| 13.4 | Результат оператора назначения не должен использоваться |
| 14.1 | Счетчик цикла не должен иметь по существу плавающего типа |
| 14.2 | A для цикла должна быть хорошо сформирована |
| 14.4 | Управляющее выражение оператора if и управляющее выражение оператора итерации должны иметь по существу логический тип |
| 15.1 | Оператор goto не должен использоваться |
| 15.2 | Оператор goto должен перейти к метке, объявленной позже в той же функции |
| 15.3 | Любая метка, на которую ссылается оператор goto, должна быть объявлена в том же блоке или в любом блоке, содержащем оператор goto |
| 15.5 | Функция должна иметь одну точку выхода в конце |
| 15.6 | Текст итерации- оператора или оператора о выборе должен быть компаунд- оператором |
| 15.7 | Все, если... другое, если конструкции должны быть завершены оператором else |
| 16.4 | Каждый оператор switch должен иметь метку по умолчанию |
| 16.5 | Метка по умолчанию должна отображаться как первая или последняя метка switch оператора 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, должны быть # defined d перед оценкой |
| 20.11 | Макропараметр, непосредственно следующий за оператором #, не должен немедленно сопровождаться оператором # # |
| 21.3 | Функции выделения и удаления памяти < stdlib.h > не должны использоваться |