#include <string.h>

/*@
  requires valid_read_string (str);
  assigns \nothing;
  behavior good:
    assumes strlen(str) > 0;
    ensures \result == str[strlen(str)-1];
  behavior bad:
    assumes strlen(str) == 0;
    ensures \result == -1;
  complete behaviors;
  disjoint behaviors;
*/
char
last_char (const char *str)
{
  size_t n = strlen (str);
  return n > 0 ? str[n-1] : -1;
}