glibc strlen specification

  /*@
    requires valid_read_string (str);
    assigns \nothing;
    ensures (\forall integer i; 0 <= i < \result ==> str[i] != '\0') &&
            str[\result] == '\0';
   */
  size_t strlen (const char *str)
  {
    ...