/*@ 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; }