Array of arrays example

[lwli11]

A tutorial on how to write the loop invariant for this example would be useful:

extern int** malloc_int_array(int size);
/*@
        spec malloc_int_array(i32 size);
        requires true;
        ensures take x =  each(u64 i; i>=0u64 &&  i < (u64) size) { Owned<int*>( array_shift<int*>(return, i)) };
@*/

extern int* malloc_int_array_single(int size);
/*@
        spec malloc_int_array_single(i32 size);
        requires true;
        ensures take x = each(u64 i; i>=0u64 &&  i < (u64) size) { Owned<int>( array_shift<int>(return, i)) };

@*/
int** test()
/*@
        requires true;
        ensures take r = each(u64 i; i>=0u64 &&  i < 3u64) { Owned<int*>( array_shift<int*>(return, i)) };

@*/
{
        int** x = malloc_int_array(3);
        for (int i=0; i<3; i++)
/*@
                inv  take x2 = each(u64 j; j>=0u64 &&  j < 3u64) { Owned<int*>( array_shift<int*>(x, j)) };

@*/
        {
                if (i>=0 && i<3){
                        /*@ extract Owned<int*>, (u64) i; @*/
                        x[i] = malloc_int_array_single(3);
                }
        }
}