X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=2020-frama-c%2F5400-timeval.html;fp=2020-frama-c%2F5400-timeval.html;h=c9ee4436809bce943f27851bbdec0bc252329383;hb=6d2dcd916aa3e435d1f8ce691127bd891fc3c69a;hp=296d28135302fddba596d550b37f9dfbf9989ded;hpb=a44fc27c4a4b02ed570dd5567ff8d309b885e904;p=libguestfs-talks.git diff --git a/2020-frama-c/5400-timeval.html b/2020-frama-c/5400-timeval.html index 296d281..c9ee443 100644 --- a/2020-frama-c/5400-timeval.html +++ b/2020-frama-c/5400-timeval.html @@ -4,27 +4,94 @@

nbdkit tvdiff_usec

+

+https://www.redhat.com/archives/libguestfs/2020-October/msg00085.html +

+ 
-  /*@
-    requires \valid_read (x) && \valid_read (y);
-    requires valid_timeval (*x) && valid_timeval (*y);
-    requires \valid (r);
-    assigns *r;
-    behavior success:
-      ensures \result == 0;
-      ensures \let diff = tv_to_microseconds (*y) - tv_to_microseconds (*x);
-              INT64_MIN <= diff <= INT64_MAX &&
-              *r == diff;
-    behavior failure:
-      ensures \result == -1;
-      ensures *r == 0;
-      ensures \let diff = tv_to_microseconds (*y) - tv_to_microseconds (*x);
-              !(INT64_MIN <= diff <= INT64_MAX);
-    complete behaviors;
-    disjoint behaviors;
-   */
-  static inline int
-  tvdiff_usec (const struct timeval *x, const struct timeval *y,
-               int64_t *r)
-  ...
+/*@
+  predicate valid_timeval (struct timeval tv) =
+    tv.tv_sec >= 0 && tv.tv_usec >= 0 && tv.tv_usec < 1000000;
+  logic integer tv_to_microseconds (struct timeval tv) =
+    tv.tv_sec * 1000000 + tv.tv_usec;
+ */
+
+#ifdef FRAMA_C
+
+/*@
+   assigns *r;
+   behavior success:
+     assumes INT64_MIN <= a + b <= INT64_MAX;
+     ensures *r == a + b;
+     ensures \result == \false;
+   behavior overflow:
+     assumes !(INT64_MIN <= a + b <= INT64_MAX);
+     ensures \result == \true;
+ */
+extern bool __builtin_add_overflow (int64_t a, int64_t b, int64_t *r);
+/*@
+   assigns *r;
+   behavior success:
+     assumes INT64_MIN <= a - b <= INT64_MAX;
+     ensures *r == a - b;
+     ensures \result == \false;
+   behavior overflow:
+     assumes !(INT64_MIN <= a - b <= INT64_MAX);
+     ensures \result == \true;
+ */
+extern bool __builtin_sub_overflow (int64_t a, int64_t b, int64_t *r);
+/*@
+   assigns *r;
+   behavior success:
+     assumes INT64_MIN <= a * b <= INT64_MAX;
+     ensures *r == a * b;
+     ensures \result == \false;
+   behavior overflow:
+     assumes !(INT64_MIN <= a * b <= INT64_MAX);
+     ensures \result == \true;
+ */
+extern bool __builtin_mul_overflow (int64_t a, int64_t b, int64_t *r);
+
+#endif /* FRAMA_C */
+
+/* Return the number of µs (microseconds) *r = *y - *x.
+ * On overflow, returns -1.
+ */
+/*@
+  requires \valid_read (x) && \valid_read (y);
+  requires valid_timeval (*x) && valid_timeval (*y);
+  requires \valid (r);
+  assigns *r;
+  behavior success:
+    assumes INT64_MIN <= tv_to_microseconds (*y) - tv_to_microseconds (*x)
+                      <= INT64_MAX;
+    ensures \result == 0;
+    ensures *r == tv_to_microseconds (*y) - tv_to_microseconds (*x);
+  behavior failure:
+    assumes !(INT64_MIN <= tv_to_microseconds (*y) - tv_to_microseconds (*x)
+                        <= INT64_MAX);
+    ensures \result == -1;
+    ensures *r == 0;
+  complete behaviors;
+  disjoint behaviors;
+ */
+static inline int
+tvdiff_usec (const struct timeval *x, const struct timeval *y,
+             int64_t *r)
+{
+  int64_t usec;
+
+  if (__builtin_sub_overflow (y->tv_sec, x->tv_sec, &usec)) {
+  overflow:
+    *r = 0;
+    return -1;
+  }
+  if (__builtin_mul_overflow (usec, 1000000, &usec))
+    goto overflow;
+  if (__builtin_add_overflow (usec, y->tv_usec - x->tv_usec, &usec))
+    goto overflow;
+
+  *r = usec;
+  return 0;
+}