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