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 | Параметр указателя в прототипе функции должен быть объявлен как указатель на const, если указатель не используется для изменения адресуемого объекта. |
17.3 | >, > =, <, < = не применяется к типам указателей, кроме тех случаев, когда они указывают на один и тот же массив. |
17.4 | Индексация массива должна быть единственно допустимой формой арифметики указателя. |
17.5 | Объявление объектов должно содержать не более 2 уровней опосредования указателя. |
17.6 | Адрес объекта с автоматическим хранением не должен быть присвоен объекту, который может сохраняться после прекращения существования объекта. |
18.3 | Область памяти не должна повторно использоваться в несвязанных целях. |
18.4 | Объединения не должны использоваться. |
20.4 | Динамическое выделение памяти «куча» не должно использоваться. |
Примечание
Программное обеспечение Polyspace не проверяет MISRA® правило 18.3.
SQO-Subset2Хорошие методы проекта обычно приводят к меньшей сложности кода, что может уменьшить количество недоказанных результатов в Polyspace Code Prover. Следующий набор правил кодирования обеспечивает применение передовых методов проекта. The 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 | Все, если еще конструкции должны содержать предложение final else |
15.3 | Конечным пунктом оператора switch является пункт по умолчанию |
16.1 | Функции не должны определяться переменным числом аргументов. |
16.2 | Функции не должны вызывать себя, прямо или косвенно. |
16.3 | Идентификаторы должны быть даны для всех параметров в объявлении прототипа функции |
16.7 | Параметр указателя в прототипе функции должен быть объявлен как указатель на const, если указатель не используется для изменения адресуемого объекта. |
16.8 | Все выходные пути из функции с непустым типом возврата должны иметь явный оператор возврата с выражением |
16.9 | Идентификатор функции должен использоваться только с предыдущим &, или со списком параметров в круглых скобках, который может быть пустым |
17.3 | >, > =, <, < = не применяется к типам указателей, кроме тех случаев, когда они указывают на один и тот же массив. |
17.4 | Индексация массива должна быть единственно допустимой формой арифметики указателя. |
17.5 | Объявление объектов должно содержать не более 2 уровней опосредования указателя. |
17.6 | Адрес объекта с автоматическим хранением не должен быть присвоен объекту, который может сохраняться после прекращения существования объекта. |
18.3 | Область памяти не должна повторно использоваться в несвязанных целях. |
18.4 | Объединения не должны использоваться. |
19.4 | Макросы C должны расширяться только на инициализатор с скобками, константу, выражение в круглых скобках, квалификатор типа, спецификатор класса памяти или конструкцию нуль |
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; }