Exponenta Banner
exponenta event banner

Пользовательское утверждение

Сбои оператора assert

расширьте все на странице

Описание

Эта проверка определяет, верен ли аргумент к макросу assert.

Аргумент к макросу assert должен быть верным, когда макрос выполняется. В противном случае прерывания выполнения программы и печать сообщение об ошибке. Polyspace® моделирует это поведение путем обработки не пройдено оператора assert как ошибки времени выполнения. Эта проверка позволяет вам обнаруживать отказавшие операторы assert перед выполнением программы.

Примеры

развернуть все

#include<stdio.h>
#define size 20

int getArrayElement();

void initialize(int* array) {
 for(int i=0;i<size;i++)
   array[i] = getArrayElement();
} 

void printElement(int* array,int index) {
 assert(index < size);
 printf("%d", array[index]);
}

int getIndex() {
 int i = size;
 return i;
}

void main() {
 int array[size];
 int index; 
 
 initialize(array);
 index = getIndex();
 printElement(array,index);
 
}

В этом примере оператор assert в printElement вызывает прерывание выполнения программы если index >= size. Оператор assert убеждается, что индекс массива не является внешними границами массивов. Если код не содержит исключительные ситуации, оператор assert должен быть зеленым. В этом примере getIndex возвращает индекс, равный size. Поэтому оператор assert кажется красным.

Исправление — Правильная причина отказа assert

Когда оператор assert будет красным, исследуйте причину исключительной ситуации. В этом примере одно возможное исправление должно обеспечить getIndex, чтобы возвратить индекс, равный size-1.

#include<stdio.h>
#define size 20

int getArrayElement();

void initialize(int* array) {
 for(int i=0;i<size;i++)
  array[i] = getArrayElement();
} 

void printElement(int* array,int index) {
 assert(index < size);
 printf("%d", array[index]);
}

int getIndex() {
 int i = size;
 return (i-1);
}

void main() {
 int array[size];
 int index;
 
 initialize(array);
 index = getIndex();
 printElement(array,index);
 
}
#include <stdlib.h>

void initialize(int*);
int getNumberOfElements();

void main() {
 int numberOfElements, *myArray;
 
 numberOfElements = getNumberOfElements();
 
 myArray = (int*)malloc(numberOfElements);
 assert(myArray!=NULL);
 
 initialize(myArray);
}

В этом примере malloc может возвратить NULL в myArray. Поэтому myArray может иметь два возможных значения:

  • myArray == NULL: условие assert является ложным.

  • myArray != NULL: условие assert верно.

Комбинирование этих двух случаев, User assertion начинает работу, оператор assert является оранжевым. После оранжевого assert Polyspace полагает, что myArray не равен NULL.

Исправление — возвращаемое значение Проверки для NULL

Одно возможное исправление должно записать индивидуально настраиваемый функциональный myMalloc, где вы всегда проверяете возвращаемое значение malloc для NULL.

#include <stdio.h>
#include <stdlib.h>

void initialize(int*);
int getNumberOfElements();

void myMalloc(int **ptr, int num) {
 *ptr = (int*)malloc(num);
 if(*ptr==NULL) {
    printf("Memory allocation error");
    exit(1);
  }
}

void main() {
 int numberOfElements, *myArray=NULL;
 
 numberOfElements = getNumberOfElements();
 
 myMalloc(&myArray,numberOfElements);
 assert(myArray!=NULL);
 
 initialize(myArray);
}
#include<stdio.h>
#include<math.h>

float getNumber();
void squareRootOfDifference(float firstNumber, float secondNumber) {
   assert(firstNumber > secondNumber);
   if(firstNumber > 0 && secondNumber > 0)
   printf("Square root = %.2f",sqrt(firstNumber-secondNumber));
}

void main() {
   double firstNumber = getNumber(), secondNumber = getNumber();
   squareRootOfDifference(firstNumber,secondNumber);
}

В этом примере оператор assert в squareRootOfDifference() вызывает прерывание выполнения программы, если firstNumber является меньше, чем secondNumber. Поскольку Polyspace не имеет достаточной информации о firstNumber и secondNumber, assert является оранжевым.

После assert, все пути к выполнению, которые вызывают оконечный отказ утверждения. Поэтому после assert, Polyspace рассматривает тот firstNumber >= secondNumber. Invalid use of standard library routine начинает работу, sqrt является зеленым.

Используйте операторы assert, чтобы помочь Polyspace определить:

  • Отношения между переменными

  • Ограничения на переменные диапазоны

Проверяйте информацию

Группа: Другой
Язык: C | C++
Акроним: ASRT

Смотрите также

Темы

Документация Polyspace Code Prover
Поддержка