Update notes for talk on Frama-C.

[libguestfs-talks.git] / 2020-frama-c / snippets / last_char.c

diff --git a/2020-frama-c/snippets/last_char.c b/2020-frama-c/snippets/last_char.c
new file mode 100644 (file)
index 0000000..69c252f
--- /dev/null
+++ b/2020-frama-c/snippets/last_char.c
@@ -0,0 +1,20 @@
+#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;
+}