qemu range_init_nofail() spec

  /*@
    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;
   */