/*@ 
  assigns \nothing;
  ensures \valid((char*)\result + (0 .. size-1));
 */
void* ptr(unsigned size);

int test1(void) {
  int *p1 = ptr(sizeof(int));
  /*@ assert \valid(p1); */
  return 0;
}

int test2(void) {
  int *p1 = ptr(sizeof(int));
  /*@ assert \valid(p1); */
}

void test3(void) {
  int *p1 = ptr(sizeof(int));
  /*@ assert \valid(p1); */
  return;
}