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

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).