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は最初のものと同じである最後の1、以外それらすべてを検証！

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要素をstructの配列の2要素に置き換えた場合、WPが成功することに注意してください。

したがって、構造体へのポインタとは何ですか？

Answer 1

これは、pとqが同じ構造体を指すことができないため、WPは最後の割り当てが(*p)を変更できないと推測できないためです。

あなたは前提追加することによって、あなたがやりたいことができます。

requires \separated(p, q);