2020-frama-c/snippets/range_size-good.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   predicate empty_range(struct Range range) =
  13     range.lob == range.upb + 1;
  14   logic integer size_of_bounds(integer lob, integer upb) =
  15     upb - lob + 1;
  16   logic integer size_of_range(struct Range range) =
  17     size_of_bounds(range.lob, range.upb);
  18 */
  19
  20 /* Get the size of range. */
  21 /*@
  22   requires \valid(range);
  23   requires valid_range(*range);
  24   requires !empty_range(*range);
  25   assigns \nothing;
  26                       // case UINT64_MAX+1 -> 0
  27   ensures \result == (uint64_t)size_of_range(*range);
  28 */
  29 static inline uint64_t range_size(const Range *range)
  30 {
  31     return range->upb - range->lob + 1;
  32 }