Iterating over struct elements

[lwli11]

Is there a possible way to write the annotations so this verifies?

Basically, I want to iterate over a list of structs, and then the internal array within the struct.

typedef struct {
        int size; // Number in cluster
        char* chars; // Array in cluster
} cluster_t;

void tester(cluster_t* clusters)
        /*@
          requires take c = each(u64 j; 0u64 <= j && j < 10u64) { Owned<cluster_t>(array_shift<cluster_t>(clusters,j)) };
          ensures take c2= each(u64 j; 0u64 <= j && j < 10u64) { Owned<cluster_t>(array_shift<cluster_t>(clusters,j)) };

          @*/
{
        for (int k=0; k<10; k++)
                /*@
                  inv take c4=  each(u64 j; 0u64 <= j && j < 10u64) { Owned<cluster_t>(array_shift<cluster_t>(clusters,j)) };
                  {clusters} unchanged;
                  @*/
                if (k>=0 && k<10){
                        /*@ extract Owned<cluster_t>, (u64) k; @*/
                        cluster_t cluster = clusters[k];
                        if (cluster.size>=0){
                                {
                                        for (int i=0; i<cluster.size; i++)
                                                /*@
                                                  inv take c3 =  each(u64 j; 0u64 <= j && j < 10u64) { Owned<cluster_t>(array_shift<cluster_t>(clusters,j)) };
                                                  take cl2 = Owned<cluster_t>(&cluster);
                                                  cluster.size>=0i32; cluster.size <=MAXi32();

                                                  take cc =  each(u64 j; 0u64 <= j && j < (u64) cluster.size) { Owned<char>(array_shift<char>(cluster.chars,j)) };
                                                  {&cluster} unchanged;
                                                  {clusters} unchanged;
                                                  @*/
                                        {
                                                if (i>=0 && i< cluster.size){
                                                        /*@ extract Owned<char>, (u64) i; @*/
                                                        char c = cluster.chars[i];
                                                }
                                        }
                                }
                        }
                }
}