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

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

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