More updates.

diff --git a/2020-frama-c/9200-alternatives.html b/2020-frama-c/9200-alternatives.html
index f594042..5969c22 100644 (file)
--- a/2020-frama-c/9200-alternatives.html
+++ b/2020-frama-c/9200-alternatives.html
@@ -17,4 +17,6 @@
 
 <li> <a href="http://compcert.inria.fr/">CompCert</a>
   is INRIA's verified C compiler (not open source).
+
+<li> <a href="https://gitlab.mpi-sws.org/iris/refinedc">RefinedC</a>
 </ul>

diff --git a/2020-frama-c/notes.txt b/2020-frama-c/notes.txt
index b7254f7..7cb905c 100644 (file)
--- a/2020-frama-c/notes.txt
+++ b/2020-frama-c/notes.txt
@@ -1,7 +1,7 @@
-16th Nov 2020
+Monday 16th Nov 2020
 Formally proving tiny bits of qemu using Frama-C
 
-[in medias res]
+\f
 
 In early October I was talking to one of the developers of Frama-C,
 which is a modular framework for verifying C programs.  It's been on
@@ -14,6 +14,19 @@ tool.
 I will provide links to tutorials etc at the end.
 
 \f
+= OVERVIEW OF FRAMA-C ECOSYSTEM =
+
+The name stands for "Framework for Static Analysis of the C language".
+
+It's modular, with a core program that reads C source code
+and turns it into Abstract Syntax Trees.  And a set of plugins
+to do static analysis by annotating these syntax trees.
+Plugins can cooperate, so analysis can be passed between
+plugins.
+
+The following slides are taken from David Mentré‘s 2016 presentation.
+
+\f
 I decided to spend a day or two last month seeing if I could formally
 prove some code inside qemu, and I arbitrarily picked one of the
 smallest pieces of code in the "util/" subdirectory:
@@ -92,22 +105,6 @@ Frama-C parsed the C code and the formal specification and machine
 checked it, and it's correct - the code is bug-free.
 
 \f
-= OVERVIEW OF FRAMA-C ECOSYSTEM =
-
-Let's interrupt this and talk about Frama-C.  The name stands
-for "Framework for Static Analysis of the C language".
-
-It's modular, with a core program that reads C source code
-and turns it into Abstract Syntax Trees.  And a set of plugins
-to do static analysis by annotating these syntax trees.
-Plugins can cooperate, so analysis can be passed between
-plugins.
-
-The following slides are taken from David Mentré‘s 2016 presentation.
-
-\f
-= BACK TO RANGE.C =
-
 Going back to what we proved so far:
 
   /*@