2020-frama-c/4000-range-is-empty-again.html

   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>
   4
   5 <h1>Back to range_is_empty()</h1>
   6
   7 <pre class="code">
   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;
  13   */</span>
  14
  15   /* Is range empty? */
  16   <span class="comment">/*@
  17     requires \valid_read(range);
  18     requires valid_range(*range);
  19     assigns \nothing;
  20     ensures \result <==> empty_range(*range);
  21    */</span>
  22   static inline bool range_is_empty(const Range *range)
  23   {
  24       return range->lob > range->upb;
  25   }
  26 </pre>
  27
  28 <pre>
  29   $ frama-c -wp -wp-rte snippets/range_is_empty.c
  30 </pre>