/* Initialize range to the empty range */
/*@
requires \valid(range);
requires valid_range(*range);
assigns *range;
ensures empty_range(*range);
*/
static inline void range_make_empty(Range *range)
{
*range = range_empty;
assert(range_is_empty(range));
}