qemu range_contains()

  /*@
    predicate value_in_range(struct Range range, uint64_t value) =
      range.lob <= value <= range.upb;
  */

  /* Does range contain val? */
  /*@
    requires \valid_read(range);
    requires valid_range(*range);
    assigns \nothing;
    ensures \result <==> value_in_range(*range, val);
   */
  static inline bool range_contains(const Range *range, uint64_t val)
  {
      return val >= range->lob && val <= range->upb;
  }