X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=2020-frama-c%2Fsnippets%2Frange_size-good.c;fp=2020-frama-c%2Fsnippets%2Frange_size-good.c;h=7343dfad6dd7add3de4ecc008cd41c322de7103b;hb=dfb5e4bcf891d3068d245d195376f54575d8655e;hp=0000000000000000000000000000000000000000;hpb=54595cfdd8aa441edb5e4738e4643f3c5fbbe471;p=libguestfs-talks.git

diff --git a/2020-frama-c/snippets/range_size-good.c b/2020-frama-c/snippets/range_size-good.c
new file mode 100644
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;
+}