/*@ 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) { ...