range_is_empty()

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

  /* Is range empty? */
  /*@
    requires \valid_read(range);
    requires valid_range(*range);
    assigns \nothing;
    ensures \result <==> empty_range(*range);
   */
  static inline bool range_is_empty(const Range *range)
  {
      return range->lob > range->upb;
  }

  $ frama-c -wp -wp-rte snippets/range_is_empty.c