WP 被指向结构的指针弄糊涂了

Question

我正在努力让 WP 验证交换 2 个结构的函数的后置条件。

typedef struct { int x; int y; } pair;

/*@
    requires \valid({p, q});
    assigns *p, *q;
    ensures *p == \old(*q);
    ensures *q == \old(*p);
*/
void swap(pair *p, pair *q);

如果我在正文中添加几个断言，WP 会验证除最后一个以外的所有断言，这与第一个相同！

void swap(pair *p, pair *q) {
    pair tmp = *p;

    *p = *q;
    //@ assert *p == \at(*q, Pre);

    *q = tmp;
    //@ assert *q == \at(*p, Pre);

    // WP is not sure anymore!
    //@ assert *p == \at(*q, Pre);
}

Phosphorus-20170501 在 Windows 和 Ubuntu 上都会发生这种情况。

请注意，如果函数将 2 个指向 int 的指针或 struct 数组的 2 个元素而不是 2 个指向 struct 的指针交换，则 WP 会成功。

那么，指向结构的指针有什么问题？

Answer 1

这是因为你没有指定p和q不能指向同一个结构，所以WP猜不到最后的赋值不能修改(*p).

你可以通过添加前提条件来做你想做的事情：

requires \separated(p, q);

WP 被指向结构的指针弄糊涂了

WP confused by pointers to struct

frama-c