Выровняйте по ширине нарушения правила кодирования Используя проверки Code Prover

Кодирующие правила являются хорошими методами, которые вы наблюдаете для безопасного и надежного кода. Используя Polyspace^® кодируя средства проверки правила, вы находите экземпляры в своем коде, которые нарушают стандарт правила кодирования, такой как MISRA^®. Если при запуске Code Prover, вы также видите результаты проверок, которые находят ошибки времени выполнения или доказывают их отсутствие. В некоторых случаях два вида результатов могут использоваться вместе для эффективного анализа. Например, можно использовать зеленую проверку Code Prover в качестве объяснения для того, чтобы не зафиксировать нарушение правила кодирования (выравнивание).

Если при запуске регистрацию MISRA в Code Prover, некоторые средства проверки используют статический анализ Code Prover под капотом, чтобы найти нарушения MISRA. Средство проверки MISRA в Code Prover более строго по сравнению с Bug Finder, потому что Code Prover отслеживает поток данных и поток управления в вашем коде. Например:

MISRA C:2012 Rule 9.1: Правило утверждает, что значение объекта с длительностью автоматического хранения не должно быть считано, прежде чем это было установлено. Code Prover использует результаты Non-initialized local variable проверяйте, чтобы определить нарушения правила.
MISRA C^®:2004 Правила 13.7: правило утверждает, что Логические операции, результаты которых являются инвариантными, не должны быть разрешены. Code Prover использует результаты Unreachable code проверяйте, чтобы идентифицировать условия, которые всегда являются TRUE или FALSE.

В некоторых других случаях средства проверки MISRA не подавляют нарушения правила даже при том, что соответствующие зеленые проверки указывают, что нарушения не имеют никакого последствия. У вас есть выбор сделать один из них:

Строго соответствуйте стандарту и зафиксируйте нарушения правила.
Вручную выровняйте по ширине нарушения правила с помощью зеленых проверок в качестве объяснения.
Установите состояние, такое как No action planned к результату и вводят зеленую проверку как объяснение в комментариях результата. Можно позже отфильтровать выровненные по ширине результаты с помощью того состояния.

Следующие разделы показывают примеры ситуаций, где можно выровнять по ширине нарушения MISRA с помощью зеленых проверок Code Prover.

Правила о преобразованиях типа данных

В некоторых случаях неявные преобразования типа данных состоят хорошо в том, если преобразование не вызывает переполнение.

В следующем примере, линия temp = var1 - var2; нарушает MISRA C:2012 Rule 10.3. Правило утверждает, что значение выражения не должно быть присвоено объекту различной существенной категории типа. Здесь, различие между двумя int переменные присвоены char переменная. Можно выровнять по ширине это конкретное нарушение правила при помощи результатов Overflow Code Prover проверять.

int func (int var1, int var2) {
    char temp;
    temp = var1 - var2;
    if (temp > 0)
        return -1;
    else
        return 1;
}

double read_meter1(void);
double read_meter2(void);

int main(char arg, char* argv[]) {
    int meter1 = (read_meter1()) * 10;
    int meter2 = (read_meter2()) * 999;
    int tol = 10;
    if((meter1 - meter2)> -tol && (meter1 - meter2) < tol)
        func(meter1, meter2);
    return 0;
}

Рассмотрите объяснение позади этого правила. Использование неявных преобразований между типами может привести к непреднамеренным результатам, включая возможную потерю значения, знака или точности. Для преобразования из int к char, потери знака или точности не может произойти. Единственной проблемой являются возможные потери значения если различие между двумя int переполнение переменных.

Запустите Code Prover на этом коде. На панели Source нажмите = в temp = var1 - var2;. Вы видите ожидаемое нарушение Правила 10.3 MISRA C:2012, но также и зеленую проверку Overflow.

Зеленая проверка указывает что преобразование из int к char не переполняется.

Можно использовать зеленую проверку переполнения в качестве объяснения, чтобы выровнять по ширине нарушение правила.

Правила об адресной арифметике с указателями

Адресная арифметика с указателями на указателях немассивов хорошо, если указатели остаются в позволенном буфере.

В следующем примере, операции ptr++ нарушает Правило 17.4 MISRA C:2004. Правило утверждает, что индексация массива должна быть единственной позволенной формой адресной арифметики с указателями. Здесь, указатель, который не является массивом, постепенно увеличивается.

#define NUM_RECORDS 3
#define NUM_CHARACTERS 6

void readchar(char);   

int main(int argc, char* argv[]) {
    char dbase[NUM_RECORDS][NUM_CHARACTERS] = { "r5cvx", "a2x5c", "g4x3c"};
    char *ptr = &dbase[0][0];
    for (int index = 0; index < NUM_RECORDS * NUM_CHARACTERS; index++) {
        readchar(*ptr);
        ptr++;
    }
    return 0;
}

Рассмотрите объяснение позади этого правила. После шага указатель может выйти за пределы границ позволенного буфера (таких как массив) или даже указать на произвольное местоположение. Адресная арифметика с указателями прекрасна пока точки указателя в позволенном буфере. Можно выровнять по ширине это конкретное нарушение правила при помощи результатов Illegally dereferenced pointer Code Prover проверять.

Запустите Code Prover на этом коде. На панели Source нажмите ++ в ptr++. Вы видите ожидаемое нарушение Правила 17.4 MISRA C:2004.

Нажмите * на операции readchar(*ptr). Вы видите зеленую проверку Illegally dereferenced pointer. Зеленая проверка указывает, что указатель указывает в позволенных границах, когда разыменовано.

Можно использовать зеленую проверку, чтобы выровнять по ширине нарушение правила.

Документация