1 <meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
2 <link rel="stylesheet" href="style.css" type="text/css"/>
3 <script src="code.js" type="text/javascript"></script>
5 <h1>range_is_empty()</h1>
8 <span class="comment">/*@
9 predicate valid_range(struct Range range) =
10 range.lob <= range.upb + 1;
11 predicate empty_range(struct Range range) =
12 range.lob == range.upb + 1;
16 <span class="comment">/*@
17 requires \valid_read(range);
18 requires valid_range(*range);
20 ensures \result <==> empty_range(*range);
22 static inline bool range_is_empty(const Range *range)
24 return range->lob > range->upb;
29 $ frama-c -wp -wp-rte snippets/range_is_empty.c