在程序运算或者数据转换的时候，由于各种数据类型有各自的范围，运算的时候，其结果如果超出这个范围，就被称之为溢出。熟悉C#的同志们应该了解用来解决溢出（Overflow）问题的checked，unchecked这两个关键字。而VCC也有类似的设定。
溢出是有规律的，有时候代码原本的设计就是要利用溢出这一特性。但是VCC（以及C#）不愿意默认程序在利用溢出，所以发生溢出的时候会报错。因此有unchecked。
#include <vcc.h> unsigned hash(unsigned char∗s, unsigned len) _(requires hread_local_array(s, len)) { unsigned i, res; for (res = 0, i = 0; i < len; ++i) res = (res + s[i])∗13; return res; }
结果会是：
Verification of hash failed.
testcase(9,11) : error VC8004: (res + s[i]) ∗ 13 might overflow.
VCC敏锐地察觉到(res + s[i]) ∗ 13这里的运算可能溢出。但是这个代码是想要利用溢出的，这时候需要使用_(unchecked)。
改成” res = _(unchecked)((res + s[i])∗13); “，上面的代码就不会报错了。
例子：
int a, b; // ... a = b + 1; _(assert a < b)
这样子，VCC要么报overflow，要么验证成功，这取决于之前的代码产生的推断。
int a, b; // ... a = _(unchecked)(b + 1）; _(assert a < b)
像这样子，他不会报错说overflow。如果他不能推断出b+1不会溢出，他会报错assertion不能保证。
以下是VCC的对于_(unchecked)E的理解：
• if the value of E lies within the range of its type, then E == _(unchecked)E;
• if x and y are unsigned, then _(unchecked)(x+y)== (x+y <= UINT_MAX ? x+y : x + y−UINT_MAX), and similarly for other types;
• if x and y are unsigned, then_(unchecked)(x−y)== (x >= y ? x− y : UINT_MAX−y + x + 1), and similarly for other types.
以上。