SE547: CBMC: Using CBMC [4/19]

Consider file:mkstring-buggy.c:

char* mkstring (char c, int size) {
  char* result = NULL;
  int i=0;
  result = (char*)(malloc((size+1)*sizeof(char)));
  for (i=0; i<size; i++) {
    result[i]=c;
  }
  result[size]=0;
  return result;
}

What is this program meant to do? What is wrong with it?