#include <stdbool.h>
#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;
*/

/* Is range empty? */
/*@
  requires \valid_read(range);
  requires valid_range(*range);
  assigns \nothing;
  ensures \result <==> empty_range(*range);
 */
static inline bool range_is_empty(const Range *range)
{
    return range->lob > range->upb;
}