frama-c - 文字の配列に注釈を追加するには?

Question

私は Frama-C の初心者で、char 配列の注釈の書き方に関するいくつかの注釈を探していました。通常、例では整数を使用しています。そのため、私が書いたことが正しいかどうかはわかりません。

私はこの機能を持っています:

    User *login(char id[25], char pass[25], User *list);

以下のような注釈を書きましたが、よくわかりません。

    /*@ requires \valid(list);
      @ requires \valid_range(id, 0, 25-1);
      @ requires \valid_range(pass, 0, 25-1);
    */