Update notes for talk on Frama-C.

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

diff --git a/2020-frama-c/snippets/range_size-good.c b/2020-frama-c/snippets/range_size-good.c
new file mode 100644 (file)
index 0000000..7343dfa
--- /dev/null
+++ b/2020-frama-c/snippets/range_size-good.c
@@ -0,0 +1,32 @@
+#include <stdint.h>
+
+struct Range {
+    uint64_t lob;
+    uint64_t upb;
+};
+typedef struct Range Range;
+
+/*@
+  predicate valid_range(struct Range range) =
+    range.lob <= range.upb + 1;
+  predicate empty_range(struct Range range) =
+    range.lob == range.upb + 1;
+  logic integer size_of_bounds(integer lob, integer upb) =
+    upb - lob + 1;
+  logic integer size_of_range(struct Range range) =
+    size_of_bounds(range.lob, range.upb);
+*/
+
+/* Get the size of range. */
+/*@
+  requires \valid(range);
+  requires valid_range(*range);
+  requires !empty_range(*range);
+  assigns \nothing;
+                      // case UINT64_MAX+1 -> 0
+  ensures \result == (uint64_t)size_of_range(*range);
+*/
+static inline uint64_t range_size(const Range *range)
+{
+    return range->upb - range->lob + 1;
+}