#include <sys/types.h>
#include "contracts.h"

size_t my_strlen(char *s) {
    size_t i;
    for(i = 0; s[i] != 0; i++) { }
    return i;
}

char* my_strcat(char *dest, char *src) {
    size_t offset = my_strlen(dest);
    size_t i = 0; // Declare here so we can use it outside of the loop
    ASSERT(0 <= i && i <= my_strlen(src));
    while(src[i] != 0)
    //@loop_invariant 0 <= i && i <= my_strlen(src);
    {
        dest[i + offset] = src[i];
        i++;
        ASSERT(0 <= i && i <= my_strlen(src));
    }
    dest[i + offset] = 0; // null-terminate
    return dest;
}