SQO-Subset1В Polyspace ® Code Prover™ следующий набор правил кодирования обычно уменьшает количество неподтвержденных результатов.
Номер правила | Описание |
|---|---|
5.2 | Идентификаторы во внутренней области не должны использовать то же имя, что и идентификатор во внешней области, и, следовательно, скрывать этот идентификатор. |
8.11 | Спецификатор статического класса хранения должен использоваться в определениях и объявлениях объектов и функций, имеющих внутреннюю связь. |
8.12 | Когда массив объявлен с внешней связью, его размер должен быть указан явно или определен неявно при инициализации. |
11.2 | Преобразование не должно выполняться между указателем на объект и любым типом, отличным от интегрального типа, другим указателем на тип объекта или указателем на пустоту. |
11.3 | Приведение не должно выполняться между типом указателя и интегральным типом. |
12.12 | Базовые битовые представления значений с плавающей запятой не должны использоваться. |
13.3 | Выражения с плавающей запятой не должны проверяться на равенство или неравенство. |
13.4 | Управляющее выражение оператора for не должно содержать никаких объектов плавающего типа. |
13.5 | Три выражения оператора for должны касаться только управления контуром. |
14.4 | Оператор goto не используется. |
14.7 | Функция должна иметь единственную точку выхода в конце функции. |
16.1 | Функции не должны определяться переменным числом аргументов. |
16.2 | Функции не должны называть себя прямо или косвенно. |
16.7 | Параметр указателя в прототипе функции должен быть объявлен как указатель на конст, если указатель не используется для изменения адресуемого объекта. |
17.3 | >, > =, <, < = не должны применяться к типам указателей, за исключением случаев, когда они указывают на один и тот же массив. |
17.4 | Индексация массива должна быть единственной допустимой формой арифметики указателя. |
17.5 | Объявление объектов должно содержать не более 2 уровней косвенности указателя. |
17.6 | Адрес объекта с автоматическим хранением не должен присваиваться объекту, который может сохраняться после прекращения существования объекта. |
18.3 | Область памяти не должна использоваться повторно в несвязанных целях. |
18.4 | Профсоюзы не используются. |
20.4 | Динамическое выделение памяти кучи не должно использоваться. |
Примечание
Программное обеспечение Polyspace не проверяет правило MISRA ® 18.3.
SQO-Subset2Оптимальные методы проектирования обычно приводят к снижению сложности кода, что может уменьшить количество недоказанных результатов в программе Polyspace Code Prover. Следующий набор правил кодирования обеспечивает применение оптимальных методов проектирования. SQO-subset2 опция проверяет правила в SQO-subset1 и некоторые дополнительные правила.
Номер правила | Описание |
|---|---|
5.2 | Идентификаторы во внутренней области не должны использовать то же имя, что и идентификатор во внешней области, и, следовательно, скрывать этот идентификатор. |
6.3 | вместо основных типов следует использовать шрифты, указывающие на размер и заметность |
8.7 | Объекты должны быть определены в объеме блока, если доступ к ним осуществляется только из одной функции |
8.11 | Спецификатор статического класса хранения должен использоваться в определениях и объявлениях объектов и функций, имеющих внутреннюю связь. |
8.12 | Когда массив объявлен с внешней связью, его размер должен быть указан явно или определен неявно при инициализации. |
9.2 | Фигурные скобки должны использоваться для указания и согласования структуры при ненулевой инициализации массивов и структур |
9.3 | В списке перечислителей конструкция = не должна использоваться для явной инициализации элементов, отличных от первого, если только все элементы не инициализированы явным образом. |
10.3 | Значение комплексного выражения целочисленного типа может быть приведено только к типу, который является более узким и имеет ту же сигнатуру, что и базовый тип выражения. |
10.5 | Побитовые операции не должны выполняться на знаковых целочисленных типах |
11.1 | Преобразование не должно выполняться между указателем на функцию и любым типом, отличным от интегрального типа |
11.2 | Преобразование не должно выполняться между указателем на объект и любым типом, отличным от интегрального типа, другим указателем на тип объекта или указателем на пустоту. |
11.3 | Приведение не должно выполняться между типом указателя и интегральным типом. |
11.5 | Отливка по типу от любого типа к указателям или от указателей не должна использоваться |
12.1 | Ограниченная зависимость от правил приоритета оператора C в выражениях |
12.2 | Значение выражения должно быть одинаковым при любом порядке оценки, который допускает стандарт |
12.5 | Операнды логического & или | | должны быть первичными выражениями |
12.6 | Операнды логических операторов (&, | | и!) должны быть логическими. Выражения, которые фактически являются логическими, не должны использоваться в качестве операндов для операторов, отличных от (&, | | или!) |
12.9 | Оператор «унарный минус» не применяется к выражению, базовый тип которого не подписан |
12.10 | Оператор запятой не должен использоваться |
12.12 | Базовые битовые представления значений с плавающей запятой не должны использоваться. |
13.1 | Операторы назначения не должны использоваться в выражениях, дающих логические значения |
13.2 | Тесты значения против нуля должны быть явными, если операнд не является логическим |
13.3 | Выражения с плавающей запятой не должны проверяться на равенство или неравенство. |
13.4 | Управляющее выражение оператора for не должно содержать никаких объектов плавающего типа. |
13.5 | Три выражения оператора for должны касаться только управления контуром. |
13.6 | Числовые переменные, используемые в цикле «for» для подсчета итераций, не должны изменяться в теле цикла |
14.4 | Оператор goto не используется. |
14.7 | Функция должна иметь единственную точку выхода в конце функции. |
14.8 | Заявление, формирующее корпус выключателя, в то время как, делает , в то время как или для заявления будет составное заявление |
14.10 | All if else, если конструкции должны содержать заключительное предложение else |
15.3 | Последний пункт заявления о переключении должен быть пунктом по умолчанию |
16.1 | Функции не должны определяться переменным числом аргументов. |
16.2 | Функции не должны называть себя прямо или косвенно. |
16.3 | Идентификаторы должны быть даны для всех параметров в объявлении прототипа функции |
16.7 | Параметр указателя в прототипе функции должен быть объявлен как указатель на конст, если указатель не используется для изменения адресуемого объекта. |
16.8 | Все пути выхода из функции с типом возврата non-void должны иметь явную инструкцию return с выражением |
16.9 | Идентификатор функции должен использоваться только с предшествующим списком параметров или со списком параметров в скобках, который может быть пустым. |
17.3 | >, > =, <, < = не должны применяться к типам указателей, за исключением случаев, когда они указывают на один и тот же массив. |
17.4 | Индексация массива должна быть единственной допустимой формой арифметики указателя. |
17.5 | Объявление объектов должно содержать не более 2 уровней косвенности указателя. |
17.6 | Адрес объекта с автоматическим хранением не должен присваиваться объекту, который может сохраняться после прекращения существования объекта. |
18.3 | Область памяти не должна использоваться повторно в несвязанных целях. |
18.4 | Профсоюзы не используются. |
19.4 | Макросы C должны расширяться только до инициализатора с скобками, константы, выражения в скобках, квалификатора типа, спецификатора класса хранения или конструкции do-while-zero. |
19.9 | Аргументы для функционального макроса не должны содержать маркеры, похожие на директивы предварительной обработки |
19.10 | В определении функционального макроса каждый экземпляр параметра должен быть заключен в круглые скобки, если он не используется в качестве операнда # или # # |
19.11 | Все идентификаторы макросов в директивах препроцессора должны быть определены перед использованием, за исключением директив # ifdef и # ifndef препроцессора и оператора defined () |
19.12 | В одном определении макроса должно присутствовать не более одного вхождения операторов препроцессора # или # #. |
20.3 | Проверяется достоверность значений, передаваемых библиотечным функциям. |
20.4 | Динамическое выделение памяти кучи не должно использоваться. |
Примечание
Программное обеспечение Polyspace не проверяет правило MISRA 20.3 напрямую.
Однако это правило можно проверить, написав заглушки вручную, которые проверяют действительность значений. Например, следующий код проверяет действительность ввода, превышающего 1:
int my_system_library_call(int in) {assert (in>1); if random \
return -1 else return 0; }