#include <string.h>

/* Return length of string */

int strlen(const char *s) NONBANKED
{
    int i;

    i = 0;
    while(*s++)
	i++;
    return i;
}