Polyspace® не проверяет следующий MISRA®C ++ кодирующие правила. Эти правила не проверяются или в Программе автоматического доказательства Средства поиска или Кода Ошибки. Некоторые из этих правил не могут быть осуществлены, потому что они выходят за рамки программного обеспечения Polyspace. Правила касаются документации, динамических аспектов или функциональных аспектов правил MISRA.
Для списка поддерживаемых правил см. MISRA C ++:2008 Правил.
| N. | Категория | Определение MISRA | Спецификация Polyspace |
|---|---|---|---|
| 0-1-4 | Необходимый | Проект не должен содержать энергонезависимые переменные POD, имеющие только одно использование. | |
| 0-1-6 | Необходимый | Проект не должен содержать экземпляры энергонезависимых переменных, даваемых значения, которые впоследствии никогда не используются. | |
| 0-1-8 | Необходимый | Все функции с пустым типом возврата должны иметь внешние побочные эффекты. | |
| 0-3-1 | Необходимый | Минимизация отказов во время выполнения должна быть обеспечена при помощи по крайней мере одного из: (a) инструментов/методов статического анализа; (b) инструментов/методов динамического анализа; (c) явного кодирования проверок, чтобы обработать отказы во время выполнения. | |
| 0-3-2 | Необходимый | Если функция сгенерирует информацию об ошибке, то та информация об ошибке должна быть протестирована. | |
| 0-4-1 | Документ | Использование масштабировано-целочисленных или вычислений с фиксированной точкой должно быть зарегистрировано. | Чтобы наблюдать это правило, проверяйте свою документацию компилятора. |
| 0-4-2 | Документ | Использование арифметики с плавающей точкой должно быть зарегистрировано. | Чтобы наблюдать это правило, проверяйте свою документацию компилятора. |
| 0-4-3 | Документ | Реализации с плавающей точкой должны выполнить заданный стандарт с плавающей точкой. | Чтобы наблюдать это правило, проверяйте свою документацию компилятора. |
| N. | Категория | Определение MISRA | Спецификация Polyspace |
|---|---|---|---|
| 1-0-2 | Документ | Несколько компиляторов должны только использоваться, если у них будет общий, заданный интерфейс. | Чтобы наблюдать это правило, проверяйте свою документацию компилятора. |
| 1-0-3 | Документ | Реализация целочисленного деления в выбранном компиляторе должна быть определена и зарегистрирована. | Чтобы наблюдать это правило, проверяйте свою документацию компилятора. |
| N. | Категория | Определение MISRA | Спецификация Polyspace |
|---|---|---|---|
| 2-2-1 | Документ | Набор символов и соответствующее кодирование должны быть зарегистрированы. | Чтобы наблюдать это правило, проверяйте свою документацию компилятора. |
| 2-7-2 | Необходимый | Разделы кода не должны быть то, " прокомментировал" использование комментариев C-стиля. | Одним путем инструмент может проверять, что это правило состоит в том, чтобы определить, компилирует ли код, когда прокомментировал разделы, не прокомментированы. Однако такая проверка может быть дорогой и неточной. |
| 2-7-3 | Консультация | Разделы кода не должны быть то, " прокомментировал" использование комментариев C++. | Одним путем инструмент может проверять, что это правило состоит в том, чтобы определить, компилирует ли код, когда прокомментировал разделы, не прокомментированы. Однако такая проверка может быть дорогой и неточной. |
| N. | Категория | Определение MISRA | Спецификация Polyspace |
|---|---|---|---|
| 5-0-16 | Необходимый | Операнд указателя и любой указатель, следующий из адресной арифметики с указателями с помощью того операнда, должны оба обратиться к элементам того же массива. | |
| 5-17-1 | Необходимый | Семантическая эквивалентность между бинарным оператором и его формой оператора присваивания должна быть сохранена. |
| N. | Определение MISRA | Спецификация Polyspace | |
|---|---|---|---|
| 7-2-1 | Необходимый | Выражение с типом лежания в основе перечисления должно только иметь значения, соответствующие перечислителям перечисления. | |
| 7-4-1 | Документ | Все использование ассемблера должно быть зарегистрировано. | Чтобы наблюдать это правило, проверяйте свою документацию компилятора. |
| N. | Категория | Определение MISRA | Спецификация Polyspace |
|---|---|---|---|
| 9-6-1 | Документ | Когда абсолютное расположение битов, представляющих битовое поле, будет требоваться, затем поведение и упаковка битовых полей должны быть зарегистрированы. | Чтобы наблюдать это правило, проверяйте свою документацию компилятора. |
| N. | Определение MISRA | Спецификация Polyspace | |
|---|---|---|---|
| 14-5-1 | Необходимый | Родовая функция лица, не являющегося членом какой-либо организации, должна только быть объявлена в пространстве имен, которое не является связанным пространством имен. | |
| 14-7-1 | Необходимый | Все шаблоны классов, шаблоны функций, функции членства шаблона класса и шаблон класса статические участники нужно инстанцировать, по крайней мере, однажды. | |
| 14-7-2 | Необходимый | Для любой данной специализации шаблона явное инстанцирование шаблона с аргументами шаблона, используемыми в специализации, не должно представлять плохо сформированную программу. |
| N. | Категория | Определение MISRA | Спецификация Polyspace |
|---|---|---|---|
| 15-0-1 | Документ | Исключения должны только использоваться в обработке ошибок. | Чтобы наблюдать это правило, проверяйте свою документацию компилятора. |
| 15-1-1 | Необходимый | Выражение присваивания оператора броска не должно самостоятельно заставлять исключение быть выданным. | |
| 15-3-1 | Необходимый | Исключения должны быть повышены только после запуска и перед завершением программы. | |
| 15-3-4 | Необходимый | Каждое исключение, явным образом добавленное, код должен иметь обработчик совместимого типа во всех путях к вызову, которые могли привести к той точке. |
| N. | Категория | Определение MISRA | Спецификация Polyspace |
|---|---|---|---|
| 17-0-3 | Необходимый | Имена стандартных библиотечных функций не должны быть заменены. | |
| 17-0-4 | Необходимый | Весь код библиотеки должен соответствовать C++ MISRA. | Чтобы наблюдать это правило, проверяйте свою документацию компилятора. |
