qemu range_make_empty()

  /* 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));
  }