verifiable-c - 前提条件の配列範囲

Question

現在VSTの使い方を勉強中です。VST1.5を使用しています。私はこの小さな C プログラム ( backref.c) を持っています:

char* rbr (char* out, int length, int dist) {
  while (length-- > 0) { out[0] = out[-dist]; out++; }
  return out;
}

私のCoqコード（簡単な事前条件と事後条件付き）は

Require Import floyd.proofauto.
Require Import backref.

Local Open Scope logic.
Local Open Scope Z.

Definition rbr_spec :=
  DECLARE _rbr
    WITH sh : share, contents : Z -> int
      PRE [ _out OF (tptr tuchar), _length OF tint, _dist OF tint ]
        PROP ()
        LOCAL ()
        SEP ()
      POST [tptr tuchar] local(fun _ => True).

out[-dist]前提条件として、 toout[-1]は読み取り可能で、out[0]toout[length-1]は書き込み可能であると言いたいです。PLCC 210 ページに条件array_at_rangeが記載されていますが、VST 1.5 では使用できないようです。これどうやってするの？