Кодирующие правила являются хорошими методами, которые вы наблюдаете для безопасного и надежного кода. Используя Polyspace®, кодирующий средства проверки правила, вы находите экземпляры в своем коде, которые нарушают стандарт правила кодирования, такой как MISRA®. Если при запуске Программу автоматического доказательства Кода, вы также видите результаты проверок, которые находят ошибки времени выполнения или доказывают их отсутствие. В некоторых случаях два вида результатов могут использоваться вместе для эффективного анализа. Например, можно использовать зеленую проверку Программы автоматического доказательства Кода в качестве объяснения для того, чтобы не зафиксировать нарушение правила кодирования (выравнивание).
Если при запуске регистрацию MISRA в Программе автоматического доказательства Кода, некоторые средства проверки используют статический анализ Программы автоматического доказательства Кода под капотом, чтобы найти нарушения MISRA. Средство проверки MISRA в Программе автоматического доказательства Кода более строго по сравнению со Средством поиска Ошибки, потому что Программа автоматического доказательства Кода отслеживает поток данных и поток управления в вашем коде. Например:
MISRA C:2012 Rule 9.1: правило утверждает, что значение объекта с длительностью автоматического хранения не должно быть считано, прежде чем это было установлено. Программа автоматического доказательства кода использует результаты проверки Non-initialized local variable определить нарушения правила.
Правило 13.7 MISRA C®:2004: правило утверждает, что Логические операции, результаты которых являются инвариантными, не должны быть разрешены. Программа автоматического доказательства кода использует результаты проверки Unreachable code идентифицировать условия, которые всегда являются TRUE или FALSE.
В некоторых других случаях средства проверки MISRA не подавляют нарушения правила даже при том, что соответствующие зеленые проверки указывают, что нарушения не имеют никакого последствия. У вас есть выбор сделать один из них:
Строго соответствуйте стандарту и зафиксируйте нарушения правила.
Вручную выровняйте по ширине нарушения правила с помощью зеленых проверок в качестве объяснения.
Установите состояние, такое как 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 переполняется.
Запустите Программу автоматического доказательства Кода на этом коде. На панели Source нажмите = in 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.
Запустите Программу автоматического доказательства Кода на этом коде. На панели Source нажмите ++ in ptr++. Вы видите ожидаемое нарушение Правила 17.4 MISRA C:2004.
Нажмите * на операции readchar(*ptr). Вы видите зеленую проверку Illegally dereferenced pointer. Зеленая проверка указывает, что указатель указывает в позволенных границах, когда разыменовано.
Можно использовать зеленую проверку, чтобы выровнять по ширине нарушение правила.