2020-frama-c/snippets/range_is_empty.c

   1 #include <stdbool.h>
   2 #include <stdint.h>
   3
   4 struct Range {
   5     uint64_t lob;
   6     uint64_t upb;
   7 };
   8 typedef struct Range Range;
   9
  10 /*@
  11   predicate valid_range(struct Range range) =
  12     range.lob <= range.upb + 1;
  13   predicate empty_range(struct Range range) =
  14     range.lob == range.upb + 1;
  15 */
  16
  17 /* Is range empty? */
  18 /*@
  19   requires \valid_read(range);
  20   requires valid_range(*range);
  21   assigns \nothing;
  22   ensures \result <==> empty_range(*range);
  23  */
  24 static inline bool range_is_empty(const Range *range)
  25 {
  26     return range->lob > range->upb;
  27 }