#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. The assert оператор гарантирует, что индекс массива не является внешними границами массива. Если код не содержит исключительных ситуаций, assert оператор должен быть зеленым. В этом примере getIndex возвращает индекс, равный size. Поэтому 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-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 может иметь два возможных значения:

Объединяя эти два случая, User assertion проверяйте на assert оператор оранжевый. После оранжевого assert, Polyspace считает, что myArray не равно 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все пути выполнения, которые вызывают сбой проверки типа «assertion», заканчиваются. Поэтому следуйте assert, Polyspace считает, что firstNumber >= secondNumber. Проверка Invalid use of standard library routine на sqrt зеленый.

Использование assert операторы, которые помогают Polyspace определить: