如何證明一個包含指針操作的斷言

Question

我試圖用frama-c的WP插件來證明一個簡單的斷言。 C代碼是從Targetlink查找表中生成的。我的目標是爲函數提供足夠的註釋，以便我可以使用生成的合約來證明調用程序的屬性。作爲第一步，我在函數的開頭附近寫了一個斷言，將常量與從解除引用的指針獲取的值進行比較，請參閱以下示例。

typedef struct MAP_Tab1DS0I2T3_b_tag { 
    int Nx; 
    const int * x_table; 
    const int * z_table; 
} MAP_Tab1DS0I2T3_b; 

int LARA_GearEnaCndn_X[9] = 
{ 
    -1, 0, 1, 2, 3, 4, 5, 6, 8 
}; 

int LARA_GearEnaCndn_Z[9] = 
{ 
    1, 0, 1, 1, 0, 0, 0, 0, 0 
}; 


MAP_Tab1DS0I2T3_b Sb218_LARA_GearEnaCndn_CUR_map = { 
    9, 
    (const int *) &(LARA_GearEnaCndn_X[0]), 
    (const int *) &(LARA_GearEnaCndn_Z[0]) 
}; 

/*@ requires x == 2; */ 
int Tab1DS0I2T3_b(const MAP_Tab1DS0I2T3_b * map, int x) 
{ 
    /* SLLocal: Default storage class for local variables | Width: 8 */ 
    int Aux_U8; 
    int Aux_U8_a; 
    int Aux_U8_b; 
    int Aux_U8_c; 

    /* SLLutLocalConst: Default storage class for local variables | Width: 32 */ 
    const int * x_table /* Scaling may differ through function reuse. */; 
    const int * z_table /* Scaling may differ through function reuse. */; 

    x_table = map->x_table; 
    z_table = map->z_table; 

    //@ assert (x < x_table[(int) (map->Nx - 1)]); 

    if (x <= *(x_table)) { 
     /* Saturation. */ 
     return z_table[0]; 
    } 
    if (x >= x_table[(int) (map->Nx - 1)]) { 
     return z_table[(int) (map->Nx - 1)]; 
    } 

    /* Linear search, start low. */ 
    x_table++; 
    while (x > *(x_table++)) { 
     z_table++; 
    } 
    x_table -= 2 /* 2. */; 
    Aux_U8 = *(z_table++); 
    Aux_U8_a = *(z_table); 

    /* Interpolation. */ 
    Aux_U8_b = (int) (((int) x) - ((int) x_table[0])); 
    Aux_U8_c = (int) (((int) x_table[1]) - ((int) x_table[0])); 
    if (Aux_U8 <= Aux_U8_a) { 
     /* Positive slope. */ 
     Aux_U8 += ((int) ((((int) (int) (Aux_U8_a - Aux_U8)) * ((int) Aux_U8_b))/
     Aux_U8_c)); 
    } 
    else { 
     /* Negative slope. */ 
     Aux_U8 -= ((int) ((((int) (int) (Aux_U8 - Aux_U8_a)) * ((int) Aux_U8_b))/
     Aux_U8_c)); 
    } 
    return Aux_U8; 
} 

有人可以給我一個提示，我需要哪些註釋成功與證明？ 從Coq證明義務的角度來看，我發現沒有公理可用於像addr_of_data或access這樣的操作，我需要重寫這些術語。此外，斷言中引用的全局變量的信息缺失。

1 subgoals 
______________________________________(1/1) 
forall x_0 map_0 : Z, 
is_sint32 x_0 -> 
forall m_0 : array data, 
x_0 = 2 -> 
forall x_table_0 : Z, 
x_table_0 = addr_of_data (access m_0 (addr_shift map_0 1)) -> 
2 < 
sint32_of_data 
    (access m_0 
    (addr_shift x_table_0 
    (as_sint32 (sint32_of_data (access m_0 (addr_shift map_0 0)) - 1)))) 

BR， 哈拉爾

Answer 1

的addr_of_data，addr_shift等exioms會自動在您的COQ-IDE的store_model.v標籤給出。

你的榜樣無處說地圖得到Sb218_LARA_GearEnaCndn_CUR_map 作爲實際參數。沒有這個說法可能是錯誤的。

現在，我不知道如何使wp利用全局初始化的顯式值作爲證明的一部分。在ACSL中有一些全局不變量，但wp似乎沒有任何處理它們。因此，我將使用明確的要求語句來獲取所需的值。

考慮下面的一組在函數頭部聲明：

/*@ requires x == 2; 
    requires map->x_table == Sb218_LARA_GearEnaCndn_CUR_map.x_table; 
    requires map->Nx == Sb218_LARA_GearEnaCndn_CUR_map.Nx; 
    requires LARA_GearEnaCndn_X[8] == 8; 
    requires Sb218_LARA_GearEnaCndn_CUR_map.Nx == 9; 
    requires Sb218_LARA_GearEnaCndn_CUR_map.x_table == LARA_GearEnaCndn_X; 
    requires Sb218_LARA_GearEnaCndn_CUR_map.z_table == LARA_GearEnaCndn_Z; 
*/ 

我能夠證明所需要的斷言。

第一個是你的。 第二個和第三個是明確擴展的*map=Sb218_LARA_GearEnaCndn_CUR_map 爲了不混亂的地址範圍。 其餘部分反映了初始值設定值。