Does cyclone perform static or dynamic checks on fat pointers?

Question

I am working my way thru Cyclone: A Safe Dialect of C for a PL class. The paper's authors explain that they've added a special 'fat' pointer that stores bounds information to prevent buffer overflows. But they don't specify if the check on this pointer is static or dynamic. The example they give seems to imply that the programmer must remember to check the size of the array in order to check that they don't exceed the buffer. This seems to open up the possibility of programming errors, just like in C. I thought the whole idea of Cyclone was to make such errors impossible. Does the language have a check? Does it just make it harder to make programming mistakes?

int strlen(const char ?s) {
    int i, n;
    if (!s) return 0;
    n = s.size; //what if the programmer forgets to do this.. or accidentally adds an n++;
    for (i = 0; i < n; i++,s++)
         if (!*s) return i;
    return n;
}

Answer 1

"Fat" pointers support pointer arithmetic with run-time bounds checking.

Obtained from Wikipedia by googling for “fat pointers”.