Обоснование нарушений правил кодирования с помощью проверок 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.

В некоторых других случаях шашки МИСРА не подавляют нарушения правил, хотя соответствующие зеленые проверки указывают на то, что эти нарушения не имеют последствий. У вас есть выбор, чтобы сделать одно из следующих:

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

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

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

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

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

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;. Вы видите ожидаемое нарушение MISRA C:2012 правила 10.3, но также и зеленую проверку Overflow.

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

Для обоснования нарушения правила можно использовать зеленую проверку переполнения.

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

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

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

#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;
}

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

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

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

Для обоснования нарушения правил можно использовать зеленый чек.

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