QCP Tutorials 内存与断言

如果C程序中定义以下结构体struct int_pair，那么很自然就可以用先前定义的swap函数交换它两个域的值。

struct int_pair {
    int a;
    int b;
};

void swap_int_pair(struct int_pair * p)
{
  swap(&(p -> a), &(p -> b));
}

我们可以沿用前面的方式来描述swap_int_pair这个C函数的规约：

void swap_int_pair(struct int_pair * p)
/*@ With x y
    Require store_int(&(p -> a), x) * store_int(&(p -> b), y)
    Ensure store_int(&(p -> a), y) * store_int(&(p -> b), x) */
{
  swap(&(p -> a), &(p -> b));
}

可以看到，QCP允许在断言中使用&(p -> a)这样的C表达式用于表述一个地址，除此之外，这个规约中的断言与swap函数的情况总体无异。

QCP目前不支持直接以结构体为函数参数的C函数验证，但是允许像上述例子那样以结构体的指针为函数参数。