From 6d2dcd916aa3e435d1f8ce691127bd891fc3c69a Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Thu, 12 Nov 2020 13:12:20 +0000 Subject: [PATCH] Reworking after run through with Paolo. --- ...frama-c.html => 1500-frama-c-core-plugins.html} | 0 ...3100-frama-c.html => 1600-frama-c-plugins.html} | 0 ...3500-frama-c.html => 1700-frama-c-history.html} | 0 ...s-empty-again.html => 2400-range-is-empty.html} | 2 +- ...-contains-1.html => 2500-range-contains-1.html} | 0 ...-contains-2.html => 2550-range-contains-2.html} | 0 ...-make-empty.html => 2600-range-make-empty.html} | 0 ...00-range-size-1.html => 2700-range-size-1.html} | 0 ...00-range-size-2.term => 2710-range-size-2.term} | 0 ...00-range-size-3.html => 2720-range-size-3.html} | 0 ...00-range-size-4.term => 2730-range-size-4.term} | 0 .../{4800-range-init.html => 2800-range-init.html} | 0 .../{4850-range-init.html => 2810-range-init.html} | 0 ...ge-init-spec.html => 2820-range-init-spec.html} | 0 ...nit-spec-2.html => 2830-range-init-spec-2.html} | 0 2020-frama-c/3200-frama-c.html | 12 --- 2020-frama-c/3300-frama-c.html | 12 --- 2020-frama-c/3400-frama-c.html | 12 --- 2020-frama-c/5400-timeval.html | 111 +++++++++++++++++---- .../{6300-strlen.html => 6100-strlen-0.html} | 0 .../{6100-strlen-1.html => 6200-strlen-1.html} | 0 .../{6200-strlen-2.html => 6300-strlen-2.html} | 0 ...0-strlen.html => 6400-strlen-kernel-proof.html} | 0 2020-frama-c/9000-conclusions-1.html | 3 +- 2020-frama-c/9200-alternatives.html | 7 +- 2020-frama-c/run | 4 +- 26 files changed, 99 insertions(+), 64 deletions(-) rename 2020-frama-c/{3000-frama-c.html => 1500-frama-c-core-plugins.html} (100%) rename 2020-frama-c/{3100-frama-c.html => 1600-frama-c-plugins.html} (100%) rename 2020-frama-c/{3500-frama-c.html => 1700-frama-c-history.html} (100%) rename 2020-frama-c/{4000-range-is-empty-again.html => 2400-range-is-empty.html} (95%) rename 2020-frama-c/{4100-range-contains-1.html => 2500-range-contains-1.html} (100%) rename 2020-frama-c/{4200-range-contains-2.html => 2550-range-contains-2.html} (100%) rename 2020-frama-c/{4300-range-make-empty.html => 2600-range-make-empty.html} (100%) rename 2020-frama-c/{4400-range-size-1.html => 2700-range-size-1.html} (100%) rename 2020-frama-c/{4500-range-size-2.term => 2710-range-size-2.term} (100%) rename 2020-frama-c/{4600-range-size-3.html => 2720-range-size-3.html} (100%) rename 2020-frama-c/{4700-range-size-4.term => 2730-range-size-4.term} (100%) rename 2020-frama-c/{4800-range-init.html => 2800-range-init.html} (100%) rename 2020-frama-c/{4850-range-init.html => 2810-range-init.html} (100%) rename 2020-frama-c/{4870-range-init-spec.html => 2820-range-init-spec.html} (100%) rename 2020-frama-c/{4890-range-init-spec-2.html => 2830-range-init-spec-2.html} (100%) delete mode 100755 2020-frama-c/3200-frama-c.html delete mode 100755 2020-frama-c/3300-frama-c.html delete mode 100755 2020-frama-c/3400-frama-c.html rename 2020-frama-c/{6300-strlen.html => 6100-strlen-0.html} (100%) rename 2020-frama-c/{6100-strlen-1.html => 6200-strlen-1.html} (100%) rename 2020-frama-c/{6200-strlen-2.html => 6300-strlen-2.html} (100%) rename 2020-frama-c/{6400-strlen.html => 6400-strlen-kernel-proof.html} (100%) diff --git a/2020-frama-c/3000-frama-c.html b/2020-frama-c/1500-frama-c-core-plugins.html similarity index 100% rename from 2020-frama-c/3000-frama-c.html rename to 2020-frama-c/1500-frama-c-core-plugins.html diff --git a/2020-frama-c/3100-frama-c.html b/2020-frama-c/1600-frama-c-plugins.html similarity index 100% rename from 2020-frama-c/3100-frama-c.html rename to 2020-frama-c/1600-frama-c-plugins.html diff --git a/2020-frama-c/3500-frama-c.html b/2020-frama-c/1700-frama-c-history.html similarity index 100% rename from 2020-frama-c/3500-frama-c.html rename to 2020-frama-c/1700-frama-c-history.html diff --git a/2020-frama-c/4000-range-is-empty-again.html b/2020-frama-c/2400-range-is-empty.html similarity index 95% rename from 2020-frama-c/4000-range-is-empty-again.html rename to 2020-frama-c/2400-range-is-empty.html index 74e52f8..5e60486 100644 --- a/2020-frama-c/4000-range-is-empty-again.html +++ b/2020-frama-c/2400-range-is-empty.html @@ -2,7 +2,7 @@ -

Back to range_is_empty()

+

range_is_empty()

   /*@
diff --git a/2020-frama-c/4100-range-contains-1.html b/2020-frama-c/2500-range-contains-1.html
similarity index 100%
rename from 2020-frama-c/4100-range-contains-1.html
rename to 2020-frama-c/2500-range-contains-1.html
diff --git a/2020-frama-c/4200-range-contains-2.html b/2020-frama-c/2550-range-contains-2.html
similarity index 100%
rename from 2020-frama-c/4200-range-contains-2.html
rename to 2020-frama-c/2550-range-contains-2.html
diff --git a/2020-frama-c/4300-range-make-empty.html b/2020-frama-c/2600-range-make-empty.html
similarity index 100%
rename from 2020-frama-c/4300-range-make-empty.html
rename to 2020-frama-c/2600-range-make-empty.html
diff --git a/2020-frama-c/4400-range-size-1.html b/2020-frama-c/2700-range-size-1.html
similarity index 100%
rename from 2020-frama-c/4400-range-size-1.html
rename to 2020-frama-c/2700-range-size-1.html
diff --git a/2020-frama-c/4500-range-size-2.term b/2020-frama-c/2710-range-size-2.term
similarity index 100%
rename from 2020-frama-c/4500-range-size-2.term
rename to 2020-frama-c/2710-range-size-2.term
diff --git a/2020-frama-c/4600-range-size-3.html b/2020-frama-c/2720-range-size-3.html
similarity index 100%
rename from 2020-frama-c/4600-range-size-3.html
rename to 2020-frama-c/2720-range-size-3.html
diff --git a/2020-frama-c/4700-range-size-4.term b/2020-frama-c/2730-range-size-4.term
similarity index 100%
rename from 2020-frama-c/4700-range-size-4.term
rename to 2020-frama-c/2730-range-size-4.term
diff --git a/2020-frama-c/4800-range-init.html b/2020-frama-c/2800-range-init.html
similarity index 100%
rename from 2020-frama-c/4800-range-init.html
rename to 2020-frama-c/2800-range-init.html
diff --git a/2020-frama-c/4850-range-init.html b/2020-frama-c/2810-range-init.html
similarity index 100%
rename from 2020-frama-c/4850-range-init.html
rename to 2020-frama-c/2810-range-init.html
diff --git a/2020-frama-c/4870-range-init-spec.html b/2020-frama-c/2820-range-init-spec.html
similarity index 100%
rename from 2020-frama-c/4870-range-init-spec.html
rename to 2020-frama-c/2820-range-init-spec.html
diff --git a/2020-frama-c/4890-range-init-spec-2.html b/2020-frama-c/2830-range-init-spec-2.html
similarity index 100%
rename from 2020-frama-c/4890-range-init-spec-2.html
rename to 2020-frama-c/2830-range-init-spec-2.html
diff --git a/2020-frama-c/3200-frama-c.html b/2020-frama-c/3200-frama-c.html
deleted file mode 100755
index 306c037..0000000
--- a/2020-frama-c/3200-frama-c.html
+++ /dev/null
@@ -1,12 +0,0 @@
-
-
-
-
-
Frama-C

-
-
-
-

-Slides from
-David Mentré’s 2016 introduction to Frama-C.
-

diff --git a/2020-frama-c/3300-frama-c.html b/2020-frama-c/3300-frama-c.html
deleted file mode 100755
index 1825037..0000000
--- a/2020-frama-c/3300-frama-c.html
+++ /dev/null
@@ -1,12 +0,0 @@
-
-
-
-
-
Frama-C

-
-
-
-

-Slides from
-David Mentré’s 2016 introduction to Frama-C.
-

diff --git a/2020-frama-c/3400-frama-c.html b/2020-frama-c/3400-frama-c.html
deleted file mode 100755
index d718096..0000000
--- a/2020-frama-c/3400-frama-c.html
+++ /dev/null
@@ -1,12 +0,0 @@
-
-
-
-
-
Frama-C

-
-
-
-

-Slides from
-David Mentré’s 2016 introduction to Frama-C.
-

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;
+}
 

diff --git a/2020-frama-c/6300-strlen.html b/2020-frama-c/6100-strlen-0.html
similarity index 100%
rename from 2020-frama-c/6300-strlen.html
rename to 2020-frama-c/6100-strlen-0.html
diff --git a/2020-frama-c/6100-strlen-1.html b/2020-frama-c/6200-strlen-1.html
similarity index 100%
rename from 2020-frama-c/6100-strlen-1.html
rename to 2020-frama-c/6200-strlen-1.html
diff --git a/2020-frama-c/6200-strlen-2.html b/2020-frama-c/6300-strlen-2.html
similarity index 100%
rename from 2020-frama-c/6200-strlen-2.html
rename to 2020-frama-c/6300-strlen-2.html
diff --git a/2020-frama-c/6400-strlen.html b/2020-frama-c/6400-strlen-kernel-proof.html
similarity index 100%
rename from 2020-frama-c/6400-strlen.html
rename to 2020-frama-c/6400-strlen-kernel-proof.html
diff --git a/2020-frama-c/9000-conclusions-1.html b/2020-frama-c/9000-conclusions-1.html
index 4426eb0..83767a2 100644
--- a/2020-frama-c/9000-conclusions-1.html
+++ b/2020-frama-c/9000-conclusions-1.html
@@ -9,7 +9,8 @@
 
 
  •  Not as hard to use as I imagined.
 
-
  •  Mostly useful for small functions.
+
  •  Mostly useful for small functions. 
    
+→ For large functions look at constructive proofs in WhyML.
 
 
  •  Forces you to think very hard about assumptions and corner cases.
 
diff --git a/2020-frama-c/9200-alternatives.html b/2020-frama-c/9200-alternatives.html
index 2469692..f594042 100644
--- a/2020-frama-c/9200-alternatives.html
+++ b/2020-frama-c/9200-alternatives.html
@@ -9,8 +9,11 @@
   is a formally verified subset of the Ada programming language
   (tagline: "You simply can't write better code").
 
-
  •  KLEE has similarities
-  but is not a formal proof system.
+
  •  TLA+
+  is useful for proving distributed systems over time.
+
+
  •  Why3 / WhyML
+  can be used for constructive proofs.
 
 
  •  CompCert
   is INRIA's verified C compiler (not open source).
diff --git a/2020-frama-c/run b/2020-frama-c/run
index 48148e4..9d0edf2 100755
--- a/2020-frama-c/run
+++ b/2020-frama-c/run
@@ -25,5 +25,5 @@ fi
 #(nothing)
 
 # Run techtalk.
-techtalk-pse "$@"
-#~/d/techtalk-pse/techtalk-pse "$@"
+#techtalk-pse "$@"
+~/d/techtalk-pse/techtalk-pse "$@"
-- 
1.8.3.1