Правила кодирования являются хорошими практиками, которые вы соблюдаете для безопасного и безопасного кода. С помощью проверки правил кодирования Polyspace ® можно найти в коде экземпляры, нарушающие стандарт правил кодирования, например MISRA ®. При выполнении программы проверки кода также отображаются результаты проверок, которые обнаруживают ошибки во время выполнения или доказывают их отсутствие. В некоторых случаях два вида результатов могут использоваться вместе для эффективного анализа. Например, можно использовать зеленую проверку проверочного кода в качестве обоснования для неустранения нарушения правила кодирования (обоснования).
При выполнении проверки MISRA в программе Code Prover некоторые шашки используют статический анализ программы Code Prover под колпаком для обнаружения нарушений MISRA. Проверка MISRA в программе Code Prover является более строгой по сравнению с программой Bug Finder, поскольку программа Code Prover точно отслеживает данные и управляет потоком в коде. Например:
MISRA C:2012 Rule 9.1Правило гласит, что значение объекта с автоматической длительностью хранения не должно считываться до его установки. Средство проверки кода использует результаты Non-initialized local variable для определения нарушений правил.
MISRA C ®: 2004 Правило 13.7: Правило гласит, что логические операции, результаты которых являются инвариантными, не допускаются. Средство проверки кода использует результаты Unreachable code для определения условий, которые всегда имеют значение true или false.
В некоторых других случаях шашки МИСРА не пресекают нарушения правил, хотя соответствующие зеленые проверки показывают, что нарушения не имеют последствий. У вас есть выбор:
Строго соответствовать стандарту и фиксировать нарушения правил.
Вручную обосновать нарушения правил с помощью зеленых проверок в качестве обоснования.
Установка статуса, например No action planned к результату и введите зеленую проверку в качестве обоснования в комментарии результата. Позже с помощью этого статуса можно будет фильтровать результаты с выравниванием.
В следующих разделах приведены примеры ситуаций, когда можно обосновать нарушения MISRA с помощью зеленых проверок проверки кода.
В некоторых случаях неявные преобразования типов данных допустимы, если преобразование не приводит к переполнению.
В следующем примере строка temp = var1 - var2; нарушает MISRA C:2012 Rule 10.3. Правило гласит, что значение выражения не должно присваиваться объекту другой категории существенного типа. Здесь разница между двумя int переменные назначены char переменная. Это нарушение правила можно обосновать с помощью результатов проверки кода. 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 переменные переполняются.
Запустите программу проверки кода для этого кода. На панели «Источник» нажмите кнопку = в temp = var1 - var2;. Вы видите ожидаемое нарушение MISRA C:2012 правила 10.3, но также зеленую проверку переполнения.
Зеленый флажок указывает, что преобразование из 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;
} |
Рассмотрим обоснование этого правила. После приращения указатель может выйти за пределы допустимого буфера (например, массива) или даже указать на произвольное местоположение. Арифметика указателя является точной до тех пор, пока указатель указывает в разрешенном буфере. Это нарушение правила можно обосновать с помощью результатов проверки кода. Illegally dereferenced pointer проверка.
Запустите программу проверки кода для этого кода. На панели «Источник» нажмите кнопку ++ в ptr++. Вы видите ожидаемое нарушение правила 17.4 MISRA C:2004.
Щелкните значок * по операции readchar(*ptr). Вы видите зеленую проверку нелегальных указателей. Зеленая проверка указывает на то, что указатель указывает в пределах допустимых границ при отмене ссылки.
Для обоснования нарушения правила можно использовать зеленую проверку.