可溼性粉劑困惑指針結構

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); 
} 

這種情況發生在Windows和Ubuntu上的Phosphorus-20170501上。

請注意，如果函數將2個指針交換爲int或2個結構數組元素，而不是2個結構指針，WP會成功。

那麼，指向struct的指針有什麼問題？

Answer 1

這是因爲您沒有指定p和q不能指向相同的結構，所以WP無法猜測最後一個分配不能修改(*p)。

你可以做你想做的，加入的前提條件：

requires \separated(p, q);