frama-c - 如何证明包含指针操作的断言

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 等 exiom 会自动在 coq-ide 的 store_model.v 选项卡中给出。

您的示例没有指出 map 获取Sb218_LARA_GearEnaCndn_CUR_map作为实际参数。如果没有这一点，断言可能是错误的。

现在，我不知道如何使 wp 利用全局初始值设定项的显式值作为证明的一部分。 ACSL 中有一些全局不变量，但 wp 似乎无论如何都没有对待它们。因此，我将使用显式的 require 语句来获取所需的值。

在函数头中给出以下一组语句:

/*@ 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 的显式扩展为了不弄乱地址范围。其余部分反射(reflect)初始值设定项值。