溢出與unchecked

在程序運算或者數據轉換的時候，因爲各類數據類型有各自的範圍，運算的時候，其結果若是超出這個範圍，就被稱之爲溢出。熟悉C#的同志們應該瞭解用來解決溢出（Overflow）問題的checked，unchecked這兩個關鍵字。而VCC也有相似的設定。

溢出是有規律的，有時候代碼本來的設計就是要利用溢出這一特性。可是VCC（以及C#）不肯意默認程序在利用溢出，因此發生溢出的時候會報錯。所以有unchecked。

#include <vcc.h> 

unsigned hash(unsigned char∗s, unsigned len) 
_(requires \thread_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.

以上。