#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 оператор отображается красным цветом.

#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 может иметь два возможных значения:

Комбинируя эти два случая, проверка утверждения пользователя на assert оператор оранжевый. После оранжевого assert, Полиспейс считает, что 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, все пути выполнения, которые вызывают сбой утверждения, завершаются. Следовательно, следуя assert, Полиспейс считает, что firstNumber >= secondNumber. Проверка недопустимости использования стандартной библиотеки sqrt зеленый.

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