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