郵資-C WP常量變量和常量數組

我想證明與郵資-C的WP插件一些C代碼，並與下面的例子有問題：郵資-C WP常量變量和常量數組

typedef unsigned char uint8_t; 

const uint8_t globalStringArray[] = "demo"; 
const int STRING_LEN = 5; 

/*@ requires \valid(src) && \valid(dest) && len < 32 ; */ 
void copyMemory(uint8_t * src, uint8_t * dest, unsigned int len); 

/*@ requires \valid(arrayParam) && len < 32 ; */ 
uint8_t func(uint8_t * arrayParam, unsigned int len) 
{ 
    uint8_t arrayBig[512] = { 0 }; 
    uint8_t * array_ptr = arrayBig; 

    copyMemory(array_ptr, arrayParam, len); 
    array_ptr = array_ptr + len; 

    copyMemory(array_ptr, globalStringArray, STRING_LEN); 
    array_ptr = array_ptr + STRING_LEN; 


    return array_ptr[0]; 
}

命令：

frama-c -wp -wp-rte test.c

我的郵資-C具有版本：鈉20150201，和alt-ERGO是0.95.2

結果是

[kernel] warning: No code nor implicit assigns clause for function copyMemory, generating default assigns from the prototype 
[rte] annotating function func 
[wp] 4 goals scheduled 
[wp] [Qed] Goal typed_func_assert_rte_mem_access : Valid 
[wp] [Qed] Goal typed_func_call_Frama_C_bzero_pre : Valid 
[wp] [Alt-Ergo] Goal typed_func_call_copyMemory_pre : Valid (275ms) (209) 
[wp] [Alt-Ergo] Goal typed_func_call_copyMemory_pre_2 : Unknown (907ms)

我注意到，當我將改變

const uint8_t globalStringArray[] = "demo"; 
const int STRING_LEN = 5;

到

uint8_t globalStringArray[] = "demo"; 
int STRING_LEN = 5;

和

/*@ requires \valid(arrayParam) && len < 32 && \valid(globalStringArray); 
    requires STRING_LEN == 5;*/ 
uint8_t func(uint8_t * arrayParam, unsigned int len) 
{

結果是

[wp] Proved goals: 4/4

但我不想依賴'需要STRING_LEN == 5;'並用'const'來證明第一個例子。如何實現這一目標？

來源

2015-10-05 bataliero1234

選項-wp-init-const將指示WP考慮到const全局確實有保持其初始值在整個程序執行（這是不是默認的，因爲，雖然這在某些時候調用未定義的行爲，一些C代碼似乎認爲const是更多的建議比綁定規則）。

然而，在這種情況下，你仍然無法證明你的先決條件，因爲它確實是假的：&globalStringArray[0]是不無效，因爲它是const數組。如果您將copyMemory的合同修改爲\valid_read(dest)，則所有內容都將通過-wp-init-const選項進行驗證。

幾個在你規範補充說明，即使他們不直接關係到你的問題：

的copyMemory的requires條款並不要求src和dest指向至少長度的有效區塊len。想必你想寫類似\valid(src+(0 .. length - 1))
我猜你應該換的src和dest的作用，因爲它是一個有點怪異傳遞一個const數組作爲dest萌發的複製功能的。
最後，請記住，使用WP，每一個被稱爲（如copyMemory這裏）函數必須拿出一個assigns條款表明該內存位置可能由被調用方進行修改

來源

2015-10-06 08:15:07 Virgile

郵資-C WP常量變量和常量數組

回答

相關問題