SQO-Subset1В Polyspace® Code Prover™ следующий набор кодирования правил будет обычно сокращать количество бездоказательных результатов.
Управляйте номером | Описание |
|---|---|
5.2 | Идентификаторы во внутреннем осциллографе не должны использовать то же имя в качестве идентификатора во внешнем осциллографе, и поэтому скрыть тот идентификатор. |
8.11 | Статический спецификатор класса памяти должен использоваться в определениях и объявлениях объектов и функций, которые имеют внутреннюю связь. |
8.12 | Когда массив будет объявлен с внешней связью, ее размер должен быть утвержден явным образом или задан неявно инициализацией. |
11.2 | Преобразование не должно выполняться между указателем на объект и любым типом кроме целочисленного типа, другим указателем на тип объекта или указателем на пустоту. |
11.3 | Бросок не должен быть выполнен между типом указателя и целочисленным типом. |
12.12 | Базовые битные представления значений с плавающей точкой не должны использоваться. |
13.3 | Выражения с плавающей точкой не должны быть протестированы на равенство или неравенство. |
13.4 | Выражение управления для оператора не должно содержать объекты типа с плавающей точкой. |
13.5 | Три выражения для оператора должны быть затронуты только с управлением циклом. |
14.4 | Оператор перехода не должен использоваться. |
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 не проверяет правило 18.3 MISRA®.
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 | Ограниченная зависимость должна быть помещена в правила приоритета оператора К в выражениях |
12.2 | Значение выражения должно быть тем же самым согласно любому порядку оценки, которую разрешает стандарт |
12.5 | Операнды логического && или || должны быть первичными выражениями |
12.6 | Операнды логических операторов (&&, || и!) должно быть эффективно булевым. Выражение, которые являются эффективно булевыми, не должно использоваться в качестве операндов к операторам кроме (&&, || или!) |
12.9 | Оператор унарный минус не должен быть применен к выражению, базовый тип которого без знака |
12.10 | Оператор запятой не должен использоваться |
12.12 | Базовые битные представления значений с плавающей точкой не должны использоваться. |
13.1 | Операторы присваивания не должны использоваться в выражениях тот урожай булевы значения |
13.2 | Тесты значения против нуля должны быть сделаны явными, если операнд не является эффективно булевым |
13.3 | Выражения с плавающей точкой не должны быть протестированы на равенство или неравенство. |
13.4 | Выражение управления для оператора не должно содержать объекты типа с плавающей точкой. |
13.5 | Три выражения для оператора должны быть затронуты только с управлением циклом. |
13.6 | Числовые переменные, используемые в “для” цикла для подсчета итерации, не должны быть изменены в теле цикла |
14.4 | Оператор перехода не должен использоваться. |
14.7 | Функция должна иметь одну точку выхода в конце функции. |
14.8 | Оператор, формирующий тело переключателя, в то время как, делает , в то время как или для оператора будет составной оператор |
14.10 | Все, если еще, если построения должны содержать итоговое выражение 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 директив препроцессору и заданного () оператор |
19.12 | Должно быть самое большее одно вхождение # или ## операторов препроцессора в одном макроопределении. |
20.3 | Валидность значений, переданных библиотечным функциям, должна проверяться. |
20.4 | Динамическое выделение памяти кучи не должно использоваться. |
Программное обеспечение Polyspace не проверяет правило 20.3 MISRA непосредственно.
Однако можно проверять это правило путем записи ручных тупиков, которые проверяют валидность значений. Например, следующий код проверяет валидность входа, являющегося больше, чем 1:
int my_system_library_call(int in) {assert (in>1); if random \
return -1 else return 0; }