/*@
axiomatic string {
  logic integer strlen_{L}(char *src)
    reads src[0..];
  axiom strlen_inside{L}:
    \forall char *src; \forall integer x; 0 <= x < strlen_(src) ==> src[x] != 0;
  axiom strlen_end{L}:
    \forall char *src; src[strlen_(src)] == 0;
  axiom strlen_pos{L}:
    \forall char *src; strlen_(src) >= 0;
}
*/

/*@
requires \valid_range(src, 0, strlen_(src));
requires strlen_(src) < 0x1000000;
ensures \result == strlen_(src);
*/
int strlen(char *src)
{
  int res = 0;
  /*@ loop invariant 0 <= res && res <= strlen_(src);
      loop variant strlen_(src) - res; */
  for (; src[res]; ++res);
  return res;
}

/*@
requires \valid_range(src, 0, strlen_(src));
requires strlen_(src) < 0x1000000;
requires \valid_range(dst, 0, strlen_(dst) + strlen_(src));
requires strlen_(dst) < 0x1000000;
requires src + strlen_(src) < dst || dst + strlen_(dst) + strlen_(src) < src;
ensures \forall integer i; 0 <= i < strlen_{Pre}(dst) ==> dst[i] == \old(dst[i]);
ensures \forall integer i; 0 <= i <= strlen_(src) ==> dst[strlen_{Pre}(dst) + i] == src[i];
*/
void strcat(char *dst, const char *src)
{
  dst += strlen(dst);
  //@ assert dst == \at(dst + strlen_(dst), Pre);
  //@ ghost int i = 0;
  /*@ loop invariant 0 <= i <= \at(strlen_(src), Pre);
      loop invariant src == \at(src, Pre) + i;
      loop invariant dst == \at(dst + strlen_(dst), Pre) + i;
      loop invariant \forall integer k; 0 <= k <= \at(strlen_(src), Pre) ==> \at(src, Pre)[k] == \at(src[k], Pre);
      loop invariant \forall integer k; 0 <= k < \at(strlen_(dst), Pre) ==> \at(dst, Pre)[k] == \at(dst[k], Pre);
      loop invariant \forall integer k; 0 <= k < i ==> \at(dst, Pre)[\at(strlen_(dst), Pre) + k] == \at(src[k], Pre);
      loop variant \at(strlen_(src), Pre) - i;
   */
  for (; *src; ++src, ++dst) {
    *dst = *src;
    //@ ghost ++i;
  }
  //@ assert i == \at(strlen_(src), Pre) == strlen_(\at(src, Pre));
  *dst = 0;
}