Кодирующие правила являются хорошими методами, которые вы наблюдаете для безопасного и надежного кода. Используя Polyspace®, кодирующий средства проверки правила, вы находите экземпляры в своем коде, которые нарушают стандарт правила кодирования, такой как MISRA®. Если при запуске Программу автоматического доказательства Кода, вы также видите результаты проверок, которые находят ошибки времени выполнения или доказывают их отсутствие. В некоторых случаях два вида результатов могут использоваться вместе для эффективного анализа. Например, можно использовать зеленую проверку Программы автоматического доказательства Кода в качестве объяснения для того, чтобы не зафиксировать нарушение правила кодирования (выравнивание).
Если при запуске регистрацию MISRA в Программе автоматического доказательства Кода, некоторые средства проверки используют статический анализ Программы автоматического доказательства Кода под капотом, чтобы найти нарушения MISRA. Средство проверки MISRA в Программе автоматического доказательства Кода более строго по сравнению с Bug Finder, потому что Программа автоматического доказательства Кода отслеживает поток данных и поток управления в вашем коде. Например:
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 нажмите = в 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 нажмите ++ в ptr++. Вы видите ожидаемое нарушение Правила 17.4 MISRA C:2004.
Нажмите * на операции readchar(*ptr). Вы видите зеленую проверку Illegally dereferenced pointer. Зеленая проверка указывает, что указатель указывает в позволенных границах, когда разыменовано.
Можно использовать зеленую проверку, чтобы выровнять по ширине нарушение правила.
