Frama-Cプリプロセッサは、\ oldをすべてのポインタ参照節に挿入します。

Question

私はFrama-C版Silicon-20161101を使用しています。 ensure節にポインタ値*xを参照するたびに、プリプロセッサは*\old(x)を不必要に挿入します。

// File swap.c: 

/*@ requires \valid(a) && \valid(b); 
    @ ensures A: *a == \old(*b) ; 
    @ ensures B: *\at(\old(b),Post) == \old(*a) ; 
    @ assigns *a,*b ; 
    @*/ 
void swap(int *a,int *b) 
{ 
    int tmp = *a ; 
    *a = *b ; 
    *b = tmp ; 
    return ; 
} 

興味深いことにframa-c swap.c -print出力

/* Generated by Frama-C */ 
/*@ requires \valid(a) ∧ \valid(b); 
    ensures A: *\old(a) ≡ \old(*b); 
    ensures B: *\old(b) ≡ \old(*a); 
    assigns *a, *b; 
*/ 
void swap(int *a, int *b) 
{ 
    int tmp; 
    tmp = *a; 
    *a = *b; 
    *b = tmp; 
    return; 
} 

で処理した場合例えば、これはまだWPプラグインによって正しいと確認されました！これは、*\old(a)が\old(a)のポスト値（これは変更されていないので、まだ同じポインタです）であると仮定していますか？これはバグですか？このためのユーザーの最終的な修正はありますか？

Answer 1

ご質問に2点あります。 \old(*a)に、間接参照でもある一方で、両方のケースでは、我々はOld状態でポインタaを評価するが、現在状態で*\old(a)で、我々逆参照それを：まず、*\old(a)は\old(*a)と混同すべきではありませんOldの状態で行われます。

第2に、仮パラメータは特別なものです：ACSLマニュアルで述べたように、関数のポストステートでは、それらが関数によって変更されていてもプリステートと同じ値を持ちますこのような次のように：

/*@ 
    requires \valid(a + 0 .. 1); 
    ensures *a == \old(*a) + 1; 
    ensures a[1] == \old(a[1]) + 1; 
*/ 
void f(int *a) { 
    *a = *a + 1; 
    a++; 
    *a = *a + 1; 
} 

ここ根拠はCがcall-by-valueセマンティクスを持っているので、外の世界はのためのローカル変数として作用する（正式に行われた内部の変更を見ることができないということですこの目的）。言い換えれば、契約に関しては、上記の例ではaに結び付けられた値が、関数の実装で何が起こったとしても、渡された実際の引数の1つです。ポインタの場合、これはポインタ自体の値にのみ適用され、ポインタが指すメモリブロックに格納された値には適用されないことに注意してください。

このセマンティクスを明示的にするために、型チェッカーは、\old内のensures節の仮パラメーターのすべての出現をラップします。

このanswerを関連する、完全には類似していない質問にしたいと思うかもしれません。