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; }