From: Richard W.M. Jones <rjones@redhat.com>
Date: Mon, 16 Nov 2020 10:55:49 +0000 (+0000)
Subject: Add summary slide about range.
X-Git-Url: http://git.annexia.org/?a=commitdiff_plain;h=9332d16bf6696137441d39ed5295dd998e70eb8d;p=libguestfs-talks.git

Add summary slide about range.
---

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 =