1

ポインターを入力として取り、ポインターが NULL でないときにその内容を使用する関数の依存関係について、ACSL 仕様を作成する必要があります。この仕様は正しいと思います：

/*@ behavior p_null:
      assumes p == \null;
      assigns \result from \nothing;
    behavior p_not_null:
      assumes p != \null;
      assigns \result from *p;
*/
int f (int * p);

しかし、私はむしろ動作を避けたいと思いますが、これが正しい（そして同等である）かどうかはわかりません：

//@ assigns \result from p, *p;
int f (int * p);

場合でも*p右の部分で使用できますか?\frompNULL

4

1 に答える 1

2

はい、できます。の右側の部分は、の値に寄与する可能性がfromある場所を示していますが、計算のために読み取る必要はありません(もちろん、そうである場合は避けたほうがよいでしょう)。補足として、Cでは暗示されていないように、動作の節についても質問が提起された可能性があります。\resultf*p\resultpNULLassignsp_not_nullp!=\null\valid(p)

それにもかかわらず、動作のないコントラクトは、動作のあるものよりもわずかに正確ではありません。これは、pisNULLが定数値である場合は返され、pis が null でない場合は、 の内容のみ*pが使用されることを示しています (assigns動作のない句では、eg を返すことができます*p+(int)p。またはでも(int)p）。

于 2013-07-23T07:24:15.240 に答える