2020-frama-c/snippets/last_char.c

   1 #include <string.h>
   2
   3 /*@
   4   requires valid_read_string (str);
   5   assigns \nothing;
   6   behavior good:
   7     assumes strlen(str) > 0;
   8     ensures \result == str[strlen(str)-1];
   9   behavior bad:
  10     assumes strlen(str) == 0;
  11     ensures \result == -1;
  12   complete behaviors;
  13   disjoint behaviors;
  14 */
  15 char
  16 last_char (const char *str)
  17 {
  18   size_t n = strlen (str);
  19   return n > 0 ? str[n-1] : -1;
  20 }