Exponenta Banner

MISRA C:2012 Dir 1.1

Любое заданное реализацией поведение, от которого зависит вывод программы, должно быть зарегистрировано и понято

Описание

Направляющее определение

Любое заданное реализацией поведение, от которого зависит вывод программы, должно быть зарегистрировано и понято.

Объяснение

Построение кода задало реализацией поведение, если стандарт C позволяет компиляторам выбирать свои собственные спецификации для построения. Полный список заданного реализацией поведения доступен в Приложении J.3 стандартного ISO/IEC 9899:1999 (C99) и в Приложении G.3 стандартного ISO/IEC 9899:1990 (C90).

Если вы понимаете и документ все заданное реализацией поведение, вас можно уверить, что весь вывод вашей программы является намеренным и не произведенный случайно.

Реализация Polyspace

Анализ обнаруживает следующие возможности заданного реализацией поведения в C99 и их дубликатов в C90. Если вы знаете поведение своей реализации компилятора, выравниваете по ширине результат анализа с соответствующими комментариями. Чтобы выровнять по ширине результат, присвойте одно из этих состояний: Justified, No action planned или Not a defect.

Совет

К массе - выравнивают по ширине все результаты, которые показывают на то же заданное реализацией поведение, используют столбец Detail на панели Results List. Кликните по заголовку столбца так, чтобы все результаты с той же записью группировались. Выберите первый результат и затем выберите последний результат при удержании клавиши Shift. Присвойте состояние одному из результатов. Если вы не видите столбец Detail, щелкните правой кнопкой по любому другому заголовку столбца и включите этот столбец.

Приложение стандарта C99 касательноПоведение, которое будет зарегистрированоКак Polyspace® Helps
J.3.2: СредаАльтернативный способ, которым может быть задана функция main.

Анализ отмечает main с помощью аргументов, и возвратите типы кроме:

int main(void) { ... }
или 
int main(int argc, char *argv[]) { ... }

Смотрите раздел 5.1.2.2.1 из Стандарта C99.

J.3.2: СредаНабор имен среды и метода для изменения списка сред используется функцией getenv.

Анализ отмечает использование функции getenv. Для этой функции необходимо знать список переменных окружения и как список изменяется.

Смотрите раздел 7.20.4.5 из Стандарта C99.

J.3.6: плавающая точкаОкругляющиеся поведения охарактеризованы нестандартными значениями FLT_ROUNDS.

Анализ отмечает включать float.h, если значения FLT_ROUNDS вне набора, {-1, 0, 1, 2, 3}. Только значения в этом наборе приводят к четко определенному поведению округления.

Смотрите раздел 5.2.4.2.2 из Стандарта C99.

J.3.6: плавающая точкаМетоды оценки охарактеризованы нестандартными отрицательными величинами FLT_EVAL_METHOD.

Анализ отмечает включать float.h, если значения FLT_EVAL_METHOD вне набора, {-1, 0, 1, 2}. Только значения в этом наборе приводят к четко определенному поведению для операций с плавающей точкой.

Смотрите раздел 5.2.4.2.2 из Стандарта C99.

J.3.6: плавающая точкаНаправление округления, когда целое число преобразовано в число с плавающей запятой, которое не может точно представлять исходное значение.

Анализ отмечает преобразования от целого числа до типов данных с плавающей точкой меньшего размера (например, 64-битный int к 32-битному float).

Смотрите раздел 6.3.1.4 из Стандарта C99.

J.3.6: плавающая точкаНаправление округления, когда число с плавающей запятой преобразовано в более узкое число с плавающей запятой.

Анализ отмечает эти преобразования:

  • double к float

  • long double к double или float

Смотрите раздел 6.3.1.5 из Стандарта C99.

J.3.6: плавающая точкаСостояние по умолчанию для прагмы FENV_ACCESS.

Анализ отмечает использование прагмы кроме:

#pragma STDC FENV_ACCESS ON
или
#pragma STDC FENV_ACCESS OFF

Смотрите раздел 7.6.1 из Стандарта C99.

J.3.6: плавающая точкаСостояние по умолчанию для прагмы FP_CONTRACT.

Анализ отмечает использование прагмы кроме:

#pragma STDC FP_CONTRACT ON
или
#pragma STDC FP_CONTRACT OFF

Смотрите раздел 7.12.2 из Стандарта C99.

J.3.11: предварительная обработка директивПоведение на каждом распознало non-STDC #pragma директива.

Анализ отмечает использование прагмы:

#pragma pp-tokens
где обрабатывающий маркерный STDC сразу не делает followpragma. Например:
#pragma FENV_ACCESS ON

Смотрите раздел 6.10.6 из Стандарта C99.

J.3.12: Библиотечные функцииПовышает ли функция feraiseexcept ''неточное'' исключение с плавающей точкой в дополнение к ''переполнению'', или ''недостаточно заполните'' исключение с плавающей точкой.

Анализ отмечает вызовы функции feraiseexcept.

Смотрите раздел 7.6.2.3 из Стандарта C99.

J.3.12: Библиотечные функцииСтроки кроме "C" и "", который может быть передан в качестве второго аргумента функции setlocale.

Анализ отмечает вызовы функции setlocale, когда ее вторым аргументом не является "C" или "".

Смотрите раздел 7.11.1.1 из Стандарта C99.

J.3.12: Библиотечные функцииТипы задали для float_t и double_t, когда значение макроса FLT_EVAL_METHOD - меньше чем 0 или больше, чем 2.

Анализ отмечает включать math.h, если FLT_EVAL_METHOD имеет значения вне набора {0,1,2}.

Смотрите раздел 7.12 из Стандарта C99.

J.3.12: Библиотечные функцииОснова 2 логарифма модуля, используемого the remquo, функционирует в сокращении частного.

Анализ отмечает вызовы remquo, remquof и функции remquol.

Смотрите раздел 7.12.10.3 из Стандарта C99.

J.3.12: Библиотечные функцииСостояние завершения, возвращенное в серверную среду abort, exit или функцией _Exit.

Анализ отмечает вызовы abort, exit или функции _Exit.

Смотрите разделы 7.20.4.1, 7.20.4.3 или 7.20.4.4 из Стандарта C99.

Поиск и устранение проблем

Если вы ожидаете нарушение правила, но не видите его, обратитесь к Кодированию Стандартных Нарушений, Не Отображенных.

Проверяйте информацию

Группа: реализация
Категория: необходимый
Категория AGC: необходимый
Язык: C90, C99

Смотрите также

Темы

Введенный в R2017b

Документация Polyspace Code Prover
Поддержка