Описание

Проблема происходит, когда ваш проект содержит код, который недостижим.

Polyspace^® Bug Finder™ и Polyspace Code Prover™ проверяют это правило кодирования по-другому. Исследования могут привести к различным результатам.

Проверка на этапе выполнения Программы автоматического доказательства Кода на недостижимый код показывает больше случаев, чем средство проверки MISRA^® для этого правила. Смотрите также. Проверка на этапе выполнения выполняет более исчерпывающий анализ. В процессе, проверка может показать некоторые экземпляры, которые не являются строго недостижимым кодом, но недостижимый только в контексте анализа. Например, в следующем коде, проверка на этапе выполнения показывает потенциальное деление на нуль в первой строке и затем удаляет нулевое значение flag для остальной части анализа. Поэтому это считает блок if недостижимым.

val=1.0/flag;
if(!flag) {}

Риск

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

Пример - код после оператора return

enum light { red, amber, red_amber, green };

enum light next_light ( enum light color )
{
    enum light res;

    switch ( color )
    {
    case red:
        res = red_amber;
        break;
    case red_amber:
        res = green;
        break;
    case green:
        res = amber;
        break;
    case amber:
        res = red;
        break;
    default:
    {
        error_handler ();
        break;
    }
    }

    res = color;
    return res;
    res = color;     /* Non-compliant */
}

В этом примере нарушено правило, потому что существует недостижимая операция после оператора return.

Описание

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

Polyspace Bug Finder обнаруживает бесполезные операции записи во время анализа.

Polyspace Code Prover не обнаруживает бесполезные операции записи. Например, если вы присваиваете значение локальной переменной, но не читаете его позже, Polyspace Code Prover не обнаруживает это бесполезное присвоение. Используйте Polyspace Bug Finder, чтобы обнаружить такие бесполезные операции записи. Для получения дополнительной информации смотрите MISRA C:2012 в Polyspace Bug Finder.

В Программе автоматического доказательства Кода можно также видеть различие в результатах на основе выбора для опции Verification level (-to). Смотрите Проверку на Кодирование Стандартных Нарушений.

Риск

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

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

Операции включающие расширения языка, такие как __asm ( "NOP" ); не рассматриваются мертвым кодом.

Пример - избыточные операции

extern volatile unsigned int v;
extern char *p;

void f ( void ) {
    unsigned int x;


    ( void ) v;      /* Compliant - Exception*/
    ( int ) v;       /* Non-compliant  */
    v >> 3;          /* Non-compliant  */

    x = 3;           /* Non-compliant - Detected in Bug Finder only */

    *p++;            /* Non-compliant  */
    ( *p )++;        /* Compliant  */
}

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

Правило не нарушено когда:

Пример - избыточный вызов функции

void g ( void ) {
               /* Compliant  */
}

void h ( void) {
     g( );     /* Non-compliant */
}

В этом примере g является пустой функцией. Хотя сама функция не нарушает правило, вызов функции нарушает правило.