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

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

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

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

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

enum light { red, amber, red_amber, green };
void report_color(enum light);
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;
    }
    }

    report_color(res);
    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) (Polyspace Code Prover). Смотрите проверку на кодирование стандартных нарушений.

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

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

Операции включающие расширения языка, такие как __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  */
}

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

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

Эта проблема происходит на if- операторы, где условие всегда верно. Этот дефект происходит только на операторах "if", которые не имеют еще-оператора.

Этот дефект показывает ненужный if- операторы, когда нет никакого различия в выполнении кода если if- оператор удален.

Ненужный if операторы часто указывают на ошибку кодирования. Возможно, if условие закодировано неправильно или if оператор не требуется вообще.

Фиксация зависит от первопричины дефекта. Например, первопричиной может быть состояние ошибки, которое проверяется дважды на том же пути к выполнению, сокращая вторую проверку.

Часто детали результата показывают последовательность событий, которые привели к дефекту. Можно реализовать закрепление на любом событии в последовательности. Если детали результата не показывают историю события, можно проследить использование, щелкните правой кнопкой по опциям по исходному коду и смотрите предыдущие связанные события. См. также Интерпретируют Результаты Bug Finder в Пользовательском интерфейсе Рабочего стола Polyspace.

Смотрите примеры мер ниже.

Если избыточное условие представляет защитные методы кодирования, и вы не хотите устранять проблему, добавлять комментарии в ваш результат или код, чтобы избежать другого анализа. Смотрите Результаты Polyspace Адреса Через Исправления ошибок или Выравнивания.

typedef enum _suit {UNKNOWN_SUIT, SPADES, HEARTS, DIAMONDS, CLUBS} suit;
suit nextcard(void);
void do_something(suit s);

void bridge(void)
{
    suit card = nextcard();
    if ((card < SPADES) || (card > CLUBS)){
        card = UNKNOWN_SUIT;
    }

    if (card < 7) {
        do_something(card);
    }
}

Тип suit перечисляется с пятью опциями. Однако условное выражение card < 7 всегда оценивает к истине потому что card может быть самое большее 5. if оператор является ненужным.

Одна возможная коррекция должна изменить если-условие в коде. В этой коррекции эти 7 изменяются на UNKNOWN_SUIT иметь отношение непосредственно к типу card.

typedef enum _suit {UNKNOWN_SUIT, SPADES, HEARTS, DIAMONDS, CLUBS} suit;
suit nextcard(void);
void do_something(suit s);

void bridge(void)
{
    suit card = nextcard();
    if ((card < SPADES) || (card > CLUBS)){
        card = UNKNOWN_SUIT;
    }

    if (card > UNKNOWN_SUIT) {
        do_something(card);
    }
}

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

typedef enum _suit {UNKNOWN_SUIT, SPADES, HEARTS, DIAMONDS, CLUBS} suit;
suit nextcard(void);
void do_something(suit s);

void bridge(void)
{
    suit card = nextcard();
    if ((card < SPADES) || (card > CLUBS)){
        card = UNKNOWN_SUIT;
    }

    do_something(card);
}

Эта проблема происходит, когда значение, присвоенное переменной, никогда не читается.

Например, вы пишете значение в переменную и затем пишете второе значение прежде, чем считать предыдущее значение. Первая операция записи избыточна.

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

Идентифицируйте причину, почему вы пишете в переменную, но не читаете ее позже. Ищите общие программные ошибки, такие как случайное чтение различной переменной с аналогичным именем.

Если вы решаете, что операция записи избыточна, удалите операцию.

void sensor_amplification(void)
{
    extern int getsensor(void);
    int level;

    level = 4 * getsensor();            
    /* Defect: Useless write */
}

После переменной level присвоен значение 4 * getsensor(), это не читается.

Одна возможная коррекция должна использовать переменную level после присвоения.

#include <stdio.h>

void sensor_amplification(void)
{
    extern int getsensor(void);
    int level;

    level = 4 * getsensor(); 
    
    /* Fix: Use level after assignment */
    printf("The value is %d", level);
    
}

Переменная level распечатан, читая новое значение.