2020-frama-c/snippets/range_size.c

   1 #include <stdint.h>
   2
   3 struct Range {
   4     uint64_t lob;
   5     uint64_t upb;
   6 };
   7 typedef struct Range Range;
   8
   9 /*@
  10   predicate valid_range(struct Range range) =
  11     range.lob <= range.upb + 1;
  12   logic integer size_of_bounds(integer lob, integer upb) =
  13     upb - lob + 1;
  14   logic integer size_of_range(struct Range range) =
  15     size_of_bounds(range.lob, range.upb);
  16 */
  17
  18 /* Get the size of range. */
  19 /*@
  20   requires \valid(range);
  21   requires valid_range(*range);
  22   assigns \nothing;
  23   ensures \result == size_of_range(*range);
  24 */
  25 static inline uint64_t range_size(const Range *range)
  26 {
  27     return range->upb - range->lob + 1;
  28 }