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