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 <pre class="code">
   8   /*@
   9     requires \valid_read (x) && \valid_read (y);
  10     requires valid_timeval (*x) && valid_timeval (*y);
  11     requires \valid (r);
  12     assigns *r;
  13     behavior success:
  14       ensures \result == 0;
  15       ensures \let diff = tv_to_microseconds (*y) - tv_to_microseconds (*x);
  16               INT64_MIN <= diff <= INT64_MAX &&
  17               *r == diff;
  18     behavior failure:
  19       ensures \result == -1;
  20       ensures *r == 0;
  21       ensures \let diff = tv_to_microseconds (*y) - tv_to_microseconds (*x);
  22               !(INT64_MIN <= diff <= INT64_MAX);
  23     complete behaviors;
  24     disjoint behaviors;
  25    */
  26   static inline int
  27   tvdiff_usec (const struct timeval *x, const struct timeval *y,
  28                int64_t *r)
  29   ...
  30 </pre>