#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;
}