2020-frama-c/5400-timeval.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>nbdkit tvdiff_usec</h1>
   6
   7 <p>
   8 <a href="https://www.redhat.com/archives/libguestfs/2020-October/msg00085.html">https://www.redhat.com/archives/libguestfs/2020-October/msg00085.html</a>
   9 </p>
  10
  11 <pre class="code">
  12 /*@
  13   predicate valid_timeval (struct timeval tv) =
  14     tv.tv_sec &gt;= 0 &amp;&amp; tv.tv_usec &gt;= 0 &amp;&amp; tv.tv_usec &lt; 1000000;
  15   logic integer tv_to_microseconds (struct timeval tv) =
  16     tv.tv_sec * 1000000 + tv.tv_usec;
  17  */
  18
  19 #ifdef FRAMA_C
  20
  21 /*@
  22    assigns *r;
  23    behavior success:
  24      assumes INT64_MIN &lt;= a + b &lt;= INT64_MAX;
  25      ensures *r == a + b;
  26      ensures \result == \false;
  27    behavior overflow:
  28      assumes !(INT64_MIN &lt;= a + b &lt;= INT64_MAX);
  29      ensures \result == \true;
  30  */
  31 extern bool __builtin_add_overflow (int64_t a, int64_t b, int64_t *r);
  32 /*@
  33    assigns *r;
  34    behavior success:
  35      assumes INT64_MIN &lt;= a - b &lt;= INT64_MAX;
  36      ensures *r == a - b;
  37      ensures \result == \false;
  38    behavior overflow:
  39      assumes !(INT64_MIN &lt;= a - b &lt;= INT64_MAX);
  40      ensures \result == \true;
  41  */
  42 extern bool __builtin_sub_overflow (int64_t a, int64_t b, int64_t *r);
  43 /*@
  44    assigns *r;
  45    behavior success:
  46      assumes INT64_MIN &lt;= a * b &lt;= INT64_MAX;
  47      ensures *r == a * b;
  48      ensures \result == \false;
  49    behavior overflow:
  50      assumes !(INT64_MIN &lt;= a * b &lt;= INT64_MAX);
  51      ensures \result == \true;
  52  */
  53 extern bool __builtin_mul_overflow (int64_t a, int64_t b, int64_t *r);
  54
  55 #endif /* FRAMA_C */
  56
  57 /* Return the number of µs (microseconds) *r = *y - *x.
  58  * On overflow, returns -1.
  59  */
  60 /*@
  61   requires \valid_read (x) &amp;&amp; \valid_read (y);
  62   requires valid_timeval (*x) &amp;&amp; valid_timeval (*y);
  63   requires \valid (r);
  64   assigns *r;
  65   behavior success:
  66     assumes INT64_MIN &lt;= tv_to_microseconds (*y) - tv_to_microseconds (*x)
  67                       &lt;= INT64_MAX;
  68     ensures \result == 0;
  69     ensures *r == tv_to_microseconds (*y) - tv_to_microseconds (*x);
  70   behavior failure:
  71     assumes !(INT64_MIN &lt;= tv_to_microseconds (*y) - tv_to_microseconds (*x)
  72                         &lt;= INT64_MAX);
  73     ensures \result == -1;
  74     ensures *r == 0;
  75   complete behaviors;
  76   disjoint behaviors;
  77  */
  78 static inline int
  79 tvdiff_usec (const struct timeval *x, const struct timeval *y,
  80              int64_t *r)
  81 {
  82   int64_t usec;
  83
  84   if (__builtin_sub_overflow (y-&gt;tv_sec, x-&gt;tv_sec, &amp;usec)) {
  85   overflow:
  86     *r = 0;
  87     return -1;
  88   }
  89   if (__builtin_mul_overflow (usec, 1000000, &amp;usec))
  90     goto overflow;
  91   if (__builtin_add_overflow (usec, y-&gt;tv_usec - x-&gt;tv_usec, &amp;usec))
  92     goto overflow;
  93
  94   *r = usec;
  95   return 0;
  96 }
  97 </pre>