2020-frama-c/2100-range-struct.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>Range type</h1>
   6
   7 <pre class="code">
   8 <span class="comment">/*
   9  * Operations on 64 bit address ranges.
  10  * Notes:
  11  * - Ranges must not wrap around 0, but can include UINT64_MAX.
  12  */</span>
  13 struct Range {
  14     <span class="comment">/*
  15      * Do not access members directly, use the functions!
  16      * A non-empty range has @lob <= @upb.
  17      * An empty range has @lob == @upb + 1.
  18      */</span>
  19     uint64_t lob;        <span class="comment">/* inclusive lower bound */</span>
  20     uint64_t upb;        <span class="comment">/* inclusive upper bound */</span>
  21 };
  22 typedef struct Range Range;
  23 </pre>
  24
  25 <pre>
  26 ┌─────┬─────────┬──────── ── ── ──
  27 │     │         │
  28 └─────┴─────────┴──────── ── ── ──
  29        ↑       ↑
  30        lob   upb
  31 </pre>