From 9332d16bf6696137441d39ed5295dd998e70eb8d Mon Sep 17 00:00:00 2001
From: "Richard W.M. Jones" <rjones@redhat.com>
Date: Mon, 16 Nov 2020 10:55:49 +0000
Subject: [PATCH] Add summary slide about range.

---
 2020-frama-c/2900-range-summary.html | 24 ++++++++++++++++++++++++
 2020-frama-c/notes.txt               |  6 ++++--
 2 files changed, 28 insertions(+), 2 deletions(-)
 create mode 100644 2020-frama-c/2900-range-summary.html

diff --git a/2020-frama-c/2900-range-summary.html b/2020-frama-c/2900-range-summary.html
new file mode 100644
index 0000000..54d3cf0
--- /dev/null
+++ b/2020-frama-c/2900-range-summary.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>Proving the qemu Range type &mdash; summary</h1>
+
+<ul>
+
+<li>
+Had to remove glib header + one function.
+
+<li>
+You can run Frama-C on the original source file.
+
+<li>
+Might need a few <code>#ifdef</code>s.
+
+<li>
+Could be integrated as part of CI.
+
+<li>
+Doesn't make sense for qemu right now.
+
+</ul>
diff --git a/2020-frama-c/notes.txt b/2020-frama-c/notes.txt
index 7cb905c..43dd078 100644
--- a/2020-frama-c/notes.txt
+++ b/2020-frama-c/notes.txt
@@ -402,8 +402,10 @@ point out a few things about the final proof:
    modifications, so it would be possible to maintain the annotations
    upstream, and run the proof checker as a CI test.
 
- - It probably doesn't make sense for qemu right now though, unless we
-   could prove more substantial pieces of code.
+ - It probably doesn't make sense for qemu right now though:
+   * concerted effort to prove more substantial pieces of code
+   * would need upstream effort to modularise qemu
+   * co-develop modules and proofs
 
 
 = POWER OF 2 =
-- 
1.8.3.1