--- /dev/null
+#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;
+}