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