Reworking after run through with Paolo.

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 (file)
--- a/2020-frama-c/4000-range-is-empty-again.html
+++ b/2020-frama-c/2400-range-is-empty.html
@@ -2,7 +2,7 @@
 <link rel="stylesheet" href="style.css" type="text/css"/>
 <script src="code.js" type="text/javascript"></script>
 
-<h1>Back to range_is_empty()</h1>
+<h1>range_is_empty()</h1>
 
 <pre class="code">
   <span class="comment">/*@

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 (executable)
index 306c037..0000000
--- a/2020-frama-c/3200-frama-c.html
+++ /dev/null
@@ -1,12 +0,0 @@
-<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
-<link rel="stylesheet" href="style.css" type="text/css"/>
-<script src="code.js" type="text/javascript"></script>
-
-<h1>Frama-C</h1>
-
-<img src="slides/slide02.png" height="75%" />
-
-<p class="attribution">
-Slides from
-<a href="https://www.cs.umd.edu/class/spring2016/cmsc838G/frama-c/introduction-to-frama-c_v2.pdf">David Mentré’s 2016 introduction to Frama-C</a>.
-</p>

diff --git a/2020-frama-c/3300-frama-c.html b/2020-frama-c/3300-frama-c.html
deleted file mode 100755 (executable)
index 1825037..0000000
--- a/2020-frama-c/3300-frama-c.html
+++ /dev/null
@@ -1,12 +0,0 @@
-<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
-<link rel="stylesheet" href="style.css" type="text/css"/>
-<script src="code.js" type="text/javascript"></script>
-
-<h1>Frama-C</h1>
-
-<img src="slides/slide03.png" height="75%" />
-
-<p class="attribution">
-Slides from
-<a href="https://www.cs.umd.edu/class/spring2016/cmsc838G/frama-c/introduction-to-frama-c_v2.pdf">David Mentré’s 2016 introduction to Frama-C</a>.
-</p>

diff --git a/2020-frama-c/3400-frama-c.html b/2020-frama-c/3400-frama-c.html
deleted file mode 100755 (executable)
index d718096..0000000
--- a/2020-frama-c/3400-frama-c.html
+++ /dev/null
@@ -1,12 +0,0 @@
-<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
-<link rel="stylesheet" href="style.css" type="text/css"/>
-<script src="code.js" type="text/javascript"></script>
-
-<h1>Frama-C</h1>
-
-<img src="slides/slide04.png" height="75%" />
-
-<p class="attribution">
-Slides from
-<a href="https://www.cs.umd.edu/class/spring2016/cmsc838G/frama-c/introduction-to-frama-c_v2.pdf">David Mentré’s 2016 introduction to Frama-C</a>.
-</p>

diff --git a/2020-frama-c/5400-timeval.html b/2020-frama-c/5400-timeval.html
index 296d281..c9ee443 100644 (file)
--- a/2020-frama-c/5400-timeval.html
+++ b/2020-frama-c/5400-timeval.html
@@ -4,27 +4,94 @@
 
 <h1>nbdkit tvdiff_usec</h1>
 
+<p>
+<a href="https://www.redhat.com/archives/libguestfs/2020-October/msg00085.html">https://www.redhat.com/archives/libguestfs/2020-October/msg00085.html</a>
+</p>
+
 <pre class="code">
-  /*@
-    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 &gt;= 0 &amp;&amp; tv.tv_usec &gt;= 0 &amp;&amp; tv.tv_usec &lt; 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 &lt;= a + b &lt;= INT64_MAX;
+     ensures *r == a + b;
+     ensures \result == \false;
+   behavior overflow:
+     assumes !(INT64_MIN &lt;= a + b &lt;= 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 &lt;= a - b &lt;= INT64_MAX;
+     ensures *r == a - b;
+     ensures \result == \false;
+   behavior overflow:
+     assumes !(INT64_MIN &lt;= a - b &lt;= 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 &lt;= a * b &lt;= INT64_MAX;
+     ensures *r == a * b;
+     ensures \result == \false;
+   behavior overflow:
+     assumes !(INT64_MIN &lt;= a * b &lt;= 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) &amp;&amp; \valid_read (y);
+  requires valid_timeval (*x) &amp;&amp; valid_timeval (*y);
+  requires \valid (r);
+  assigns *r;
+  behavior success:
+    assumes INT64_MIN &lt;= tv_to_microseconds (*y) - tv_to_microseconds (*x)
+                      &lt;= INT64_MAX;
+    ensures \result == 0;
+    ensures *r == tv_to_microseconds (*y) - tv_to_microseconds (*x);
+  behavior failure:
+    assumes !(INT64_MIN &lt;= tv_to_microseconds (*y) - tv_to_microseconds (*x)
+                        &lt;= 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-&gt;tv_sec, x-&gt;tv_sec, &amp;usec)) {
+  overflow:
+    *r = 0;
+    return -1;
+  }
+  if (__builtin_mul_overflow (usec, 1000000, &amp;usec))
+    goto overflow;
+  if (__builtin_add_overflow (usec, y-&gt;tv_usec - x-&gt;tv_usec, &amp;usec))
+    goto overflow;
+
+  *r = usec;
+  return 0;
+}
 </pre>

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 (file)
--- a/2020-frama-c/9000-conclusions-1.html
+++ b/2020-frama-c/9000-conclusions-1.html
@@ -9,7 +9,8 @@
 
 <li> Not as hard to use as I imagined.
 
-<li> Mostly useful for small functions.
+<li> Mostly useful for small functions. <br>
+<big>→</big> For large functions look at constructive proofs in WhyML.
 
 <li> 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 (file)
--- 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: <i>"You simply can't write better code"</i>).
 
-<li> <a href="http://klee.github.io/">KLEE</a> has similarities
-  but is not a formal proof system.
+<li> <a href="https://lamport.azurewebsites.net/tla/tla.html">TLA+</a>
+  is useful for proving distributed systems over time.
+
+<li> <a href="http://why3.lri.fr">Why3 / WhyML</a>
+  can be used for constructive proofs.
 
 <li> <a href="http://compcert.inria.fr/">CompCert</a>
   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 (executable)
--- 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 "$@"