New empty_range and total_range predicates

  /*@ // before:
    predicate empty_range(struct Range range) =
      range.lob == range.upb + 1;
  */

  /*@ // after:
    predicate empty_range(struct Range range) =
      range.lob > 0 && range.lob == range.upb + 1;

    predicate total_range(struct Range range) =
      range.lob == 0 && range.upb == UINT64_MAX;
  */