/*@ requires \valid(range); requires lob + (integer)size <= UINT64_MAX; assigns *range; behavior empty: assumes lob > 0 && size == 0; ensures empty_range(*range); behavior non_empty: assumes size > 0; ensures range->lob == lob; ensures size_of_bounds(lob, range->upb) == size; behavior total: assumes lob == 0 && size == 0; ensures total_range(*range); complete behaviors; disjoint behaviors; */