ユーザー アサーション

assert ステートメントが失敗

このページをすべて展開する

説明

このチェックでは、assert マクロの引数が true かどうかを判別します。

assert マクロの引数は、このマクロの実行時には true でなければなりません。それ以外の場合はプログラムが中止し、エラー メッセージが出力されます。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);
 
}

この例では、printElement 内の assert ステートメントが原因となり、index >= size の場合にプログラムが中止します。assert ステートメントは、配列インデックスが配列の境界外とならないようにしています。コードに例外的な状況が含まれていない場合、assert ステートメントはグリーンになるはずです。この例では、getIndex が size に等しいインデックスを返します。したがって、assert ステートメントは赤で表示されます。

修正 — assert の失敗の原因を訂正

assert ステートメントが赤の場合は、例外的状況の原因を調べてください。この例では、1 つの修正方法として、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 は次の 2 つの値をもつ可能性があります。

  • myArray == NULL:assert の条件が false。

  • myArray != NULL:assert の条件が true。

この 2 つのケースを結合して、assert ステートメントに対する [ユーザー アサーション] チェックはオレンジになります。オレンジの assert の後、Polyspace は myArray が NULL に等しくないとみなします。

修正 — NULL の戻り値をチェック

1 つの修正方法として、カスタマイズされた関数 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);
}

この例では、squareRootOfDifference() 内の assert ステートメントが原因となり、firstNumber が secondNumber より小さい場合にプログラムが中止します。Polyspace には firstNumber と secondNumber についての十分な情報がないため、assert はオレンジになります。

assert の後、アサーションの失敗の原因となるすべての実行パスは終了します。したがって、assert の後、Polyspace では firstNumber >= secondNumber であるとみなします。sqrt に対する [標準ライブラリ ルーチンの無効な使用] チェックはグリーンになります。

assert ステートメントを使用して、Polyspace での以下の判別に役立ててください。

  • 変数間の関係

  • 変数範囲に対する制約

チェック情報

グループ: Other
言語: C | C++
頭字語: ASRT

参考

トピック