function strlen(arg0)
{
    return string_length(arg0);
}