4 requires valid_read_string (str);
7 assumes strlen(str) > 0;
8 ensures \result == str[strlen(str)-1];
10 assumes strlen(str) == 0;
11 ensures \result == -1;
16 last_char (const char *str)
18 size_t n = strlen (str);
19 return n > 0 ? str[n-1] : -1;