cyclone是对fat指针执行静态检查还是动态检查？

Question

我正在通过Cyclone: A Safe Dialect of C学习一个PL类。这篇论文的作者解释说，他们已经添加了一个特殊的“胖”指针来存储边界信息，以防止缓冲区溢出。但是他们没有指定这个指针上的检查是静态的还是动态的。他们给出的例子似乎暗示程序员必须记得检查数组的大小，以便检查它们是否没有超过缓冲区。这似乎打开了编程错误的可能性，就像在C中一样。我认为Cyclone的整个想法就是让这种错误变得不可能。语言有检查吗？这只会让犯编程错误变得更难吗？

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

“胖”指针支持带运行时边界检查的指针算法。

通过谷歌搜索“胖指针”从Wikipedia获得。