Slides for 4xxx.

diff --git a/2020-frama-c/4000-range-is-empty-again.html b/2020-frama-c/4000-range-is-empty-again.html
new file mode 100644 (file)
index 0000000..74e52f8
--- /dev/null
+++ b/2020-frama-c/4000-range-is-empty-again.html
@@ -0,0 +1,30 @@
+<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>Back to range_is_empty()</h1>
+
+<pre class="code">
+  <span class="comment">/*@
+    predicate valid_range(struct Range range) =
+      range.lob <= range.upb + 1;
+    predicate empty_range(struct Range range) =
+      range.lob == range.upb + 1;
+  */</span>
+
+  /* Is range empty? */
+  <span class="comment">/*@
+    requires \valid_read(range);
+    requires valid_range(*range);
+    assigns \nothing;
+    ensures \result <==> empty_range(*range);
+   */</span>
+  static inline bool range_is_empty(const Range *range)
+  {
+      return range->lob > range->upb;
+  }
+</pre>
+
+<pre>
+  $ frama-c -wp -wp-rte snippets/range_is_empty.c
+</pre>

diff --git a/2020-frama-c/4100-range-contains-1.html b/2020-frama-c/4100-range-contains-1.html
new file mode 100644 (file)
index 0000000..91403c9
--- /dev/null
+++ b/2020-frama-c/4100-range-contains-1.html
@@ -0,0 +1,13 @@
+<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>qemu range_contains()</h1>
+
+<pre class="code">
+  /* Does range contain val? */
+  static inline bool range_contains(const Range *range, uint64_t val)
+  {
+      return val >= range->lob && val <= range->upb;
+  }
+</pre>

diff --git a/2020-frama-c/4200-range-contains-2.html b/2020-frama-c/4200-range-contains-2.html
new file mode 100644 (file)
index 0000000..f64bb7e
--- /dev/null
+++ b/2020-frama-c/4200-range-contains-2.html
@@ -0,0 +1,24 @@
+<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>qemu range_contains()</h1>
+
+<pre class="code">
+  <span class="comment">/*@
+    predicate value_in_range(struct Range range, uint64_t value) =
+      range.lob <= value <= range.upb;
+  */</span>
+
+  /* Does range contain val? */
+  <span class="comment">/*@
+    requires \valid_read(range);
+    requires valid_range(*range);
+    assigns \nothing;
+    ensures \result <==> value_in_range(*range, val);
+   */</span>
+  static inline bool range_contains(const Range *range, uint64_t val)
+  {
+      return val >= range->lob && val <= range->upb;
+  }
+</pre>

diff --git a/2020-frama-c/4300-range-make-empty.html b/2020-frama-c/4300-range-make-empty.html
new file mode 100644 (file)
index 0000000..ec8fe4c
--- /dev/null
+++ b/2020-frama-c/4300-range-make-empty.html
@@ -0,0 +1,20 @@
+<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>qemu range_make_empty()</h1>
+
+<pre class="code">
+  /* Initialize range to the empty range */
+  <span class="comment">/*@
+    requires \valid(range);
+    requires valid_range(*range);
+    assigns *range;
+    ensures empty_range(*range);
+   */</span>
+  static inline void range_make_empty(Range *range)
+  {
+      *range = range_empty;
+      assert(range_is_empty(range));
+  }
+</pre>

diff --git a/2020-frama-c/4400-range-size-1.html b/2020-frama-c/4400-range-size-1.html
new file mode 100644 (file)
index 0000000..8af73b1
--- /dev/null
+++ b/2020-frama-c/4400-range-size-1.html
@@ -0,0 +1,13 @@
+<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>qemu range_size()</h1>
+
+<pre class="code">
+  /* Get the size of range. */
+  static inline uint64_t range_size(const Range *range)
+  {
+      return range->upb - range->lob + 1;
+  }
+</pre>

diff --git a/2020-frama-c/4500-range-size-2.term b/2020-frama-c/4500-range-size-2.term
new file mode 100755 (executable)
index 0000000..7c4b874
--- /dev/null
+++ b/2020-frama-c/4500-range-size-2.term
@@ -0,0 +1,12 @@
+#!/bin/bash -
+
+source functions
+
+# Title.
+export title="qemu’s range_size()"
+
+# History.
+remember 'cat snippets/range_size.c'
+remember 'frama-c -wp -wp-rte snippets/range_size.c'
+
+terminal

diff --git a/2020-frama-c/4600-range-size-3.html b/2020-frama-c/4600-range-size-3.html
new file mode 100644 (file)
index 0000000..28e5f5f
--- /dev/null
+++ b/2020-frama-c/4600-range-size-3.html
@@ -0,0 +1,19 @@
+<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>qemu range_size() counterexample</h1>
+
+<pre class="code">
+  /* Get the size of range. */
+  static inline uint64_t range_size(const Range *range)
+  {
+      return range->upb - range->lob + 1;
+  }
+</pre>
+<pre>
+  ┌─────────────────────────────────────────────────┐ 
+  │░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░│
+  └─────────────────────────────────────────────────┘
+  range->lob == 0           range->upb == UINT64_MAX
+</pre>

diff --git a/2020-frama-c/4700-range-size-4.term b/2020-frama-c/4700-range-size-4.term
new file mode 100755 (executable)
index 0000000..ade027b
--- /dev/null
+++ b/2020-frama-c/4700-range-size-4.term
@@ -0,0 +1,12 @@
+#!/bin/bash -
+
+source functions
+
+# Title.
+export title="qemu’s range_size()"
+
+# History.
+remember 'cat snippets/range_size-good.c'
+remember 'frama-c -wp -wp-rte snippets/range_size-good.c'
+
+terminal

diff --git a/2020-frama-c/4800-range-init.html b/2020-frama-c/4800-range-init.html
new file mode 100644 (file)
index 0000000..8b30bc9
--- /dev/null
+++ b/2020-frama-c/4800-range-init.html
@@ -0,0 +1,18 @@
+<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>qemu range_init_nofail()</h1>
+
+<pre class="code">
+  /*
+   * Initialize range to span the interval [lob,lob + size - 1].
+   * size may be 0. Range must not overflow.
+   */
+  static inline void range_init_nofail(Range *range, uint64_t lob,
+                                       uint64_t size)
+  {
+      range->lob = lob;
+      range->upb = lob + size - 1;
+  }
+</pre>

diff --git a/2020-frama-c/4850-range-init.html b/2020-frama-c/4850-range-init.html
new file mode 100644 (file)
index 0000000..3e9d01e
--- /dev/null
+++ b/2020-frama-c/4850-range-init.html
@@ -0,0 +1,30 @@
+<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>qemu range_init_nofail()</h1>
+
+<pre class="code">
+  /*
+   * Initialize range to span the interval [lob,lob + size - 1].
+   * size may be 0. Range must not overflow.
+   */
+  static inline void range_init_nofail(Range *range, uint64_t lob,
+                                       uint64_t size)
+  {
+      range->lob = lob;
+      range->upb = lob + size - 1;
+  }
+</pre>
+<pre>
+  lob == 0  size == 0
+  ┌─────────────────────────────────────────────────┐ 
+  │░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░│
+  └─────────────────────────────────────────────────┘
+</pre>
+<pre>
+  lob == 1  size == 0
+  ┌─────────────────────────────────────────────────┐ 
+  │ │                                               │
+  └─────────────────────────────────────────────────┘
+</pre>

diff --git a/2020-frama-c/4870-range-init-spec.html b/2020-frama-c/4870-range-init-spec.html
new file mode 100644 (file)
index 0000000..a676f66
--- /dev/null
+++ b/2020-frama-c/4870-range-init-spec.html
@@ -0,0 +1,25 @@
+<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>qemu range_init_nofail() spec</h1>
+
+<pre class="code">
+  /*@
+    requires \valid(range);
+    requires lob + (integer)size <= UINT64_MAX;
+    assigns *range;
+    behavior empty:
+      assumes lob > 0 && size == 0;
+      ensures empty_range(*range);
+    behavior non_empty:
+      assumes size > 0;
+      ensures range->lob == lob;
+      ensures size_of_bounds(lob, range->upb) == size;
+    behavior total:
+      assumes lob == 0 && size == 0;
+      ensures total_range(*range);
+    complete behaviors;
+    disjoint behaviors;
+   */
+</pre>

diff --git a/2020-frama-c/4890-range-init-spec-2.html b/2020-frama-c/4890-range-init-spec-2.html
new file mode 100644 (file)
index 0000000..0db511f
--- /dev/null
+++ b/2020-frama-c/4890-range-init-spec-2.html
@@ -0,0 +1,22 @@
+<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>New empty_range and total_range predicates</h1>
+
+<pre class="code">
+  /*@ // before:
+    predicate empty_range(struct Range range) =
+      range.lob == range.upb + 1;
+  */
+</pre>
+
+<pre class="code">
+  /*@ // after:
+    predicate empty_range(struct Range range) =
+      range.lob > 0 && range.lob == range.upb + 1;
+
+    predicate total_range(struct Range range) =
+      range.lob == 0 && range.upb == UINT64_MAX;
+  */
+</pre>