Range predicates

    /*
     * Do not access members directly, use the functions!
     * A non-empty range has @lob <= @upb.
     * An empty range has @lob == @upb + 1.
     */

  /*@
    predicate valid_range(struct Range range) =
      range.lob <= range.upb + 1;

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