7 typedef struct Range Range;
10 predicate valid_range(struct Range range) =
11 range.lob <= range.upb + 1;
12 predicate empty_range(struct Range range) =
13 range.lob == range.upb + 1;
14 logic integer size_of_bounds(integer lob, integer upb) =
16 logic integer size_of_range(struct Range range) =
17 size_of_bounds(range.lob, range.upb);
20 /* Get the size of range. */
22 requires \valid(range);
23 requires valid_range(*range);
24 requires !empty_range(*range);
26 // case UINT64_MAX+1 -> 0
27 ensures \result == (uint64_t)size_of_range(*range);
29 static inline uint64_t range_size(const Range *range)
31 return range->upb - range->lob + 1;