溢出無效斷言檢查郵資-C

Question

當檢查用於加法運算short和char數據類型的溢流，通過郵資-C插入斷言是似乎是不正確的：

對於char和短數據的最大正值和負值是整型數據類型。

這可能是什麼原因？

Answer 1

在算術運算中使用時，小於int的積分類型轉換爲int或unsigned（請參見C11 6.3.1.8常規算術轉換）。這就是爲什麼你看到演員(int)爲x和y。請注意，默認情況下，-rte不會對downcast發出警告，因爲它們不是未定義的行爲（6.3.1.3§3表示已簽名的downcast是實現定義的，並且實現可能會引發信號）。如果添加的選項-warn-signed-downcast，你會看到你很可能尋找的斷言，這是由於投進去結果(char)：

/*@ assert rte: signed_downcast: (int)x+(int)y ≤ 127; */ 
/*@ assert rte: signed_downcast: -128 ≤ (int)x+(int)y; */ 

請注意，如果你把結果存儲到一個int，作爲在

void main(void) { 
    char x; 
    char y; 
    int z; 
    x = 1; 
    y = 127; 
    z = x + y; 
    return; 
} 

不會有任何下降警告（但會出現簽名溢出警告）。