SE547: CBMC: CBMC Features [16/19]

CBMC handles arrays and memory management, for example:

void sort (int* array, int size) {
  int tmp; int i; int j;
  for (i=0; i<size; i++) {
    for (j=i; j<size; j++) {
      if (array[i] > array[j]) {
        tmp = array[i];	array[i] = array[j]; array[j] = tmp;
      }
    }
  }
}

void test (int size) {
  int* array = (int*)(malloc(size*sizeof(int)));
  sort (array, size);
}

Includes tests for array bounds! file:sort.c