// mem.in2 // experimenting with arrays of owner pointers int * owner malloc(); void free(int * owner p); void f1() { int * owner p[5]; // (auto) array of 5 owner pointers int i; // here, 'p' is INTLOOP(i,5) { // for(i=0; i<5; i++) // invariant: 'p' is p[i] = malloc(); // here, 'p' is if (!p[i]) { // 'p' is abort(); // 'p' is top /* for (j=0; j } // here, 'p' is }