X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=2020-frama-c%2Fnotes.txt;fp=2020-frama-c%2Fnotes.txt;h=7cb905c2caa07de81df75443d7262dfca5e7f271;hb=358f880cc5c65bc6ef083ac1e5397e18ffd0fcce;hp=b7254f76685575b2668868d530c3ef369ed4e8a8;hpb=6d2dcd916aa3e435d1f8ce691127bd891fc3c69a;p=libguestfs-talks.git

diff --git a/2020-frama-c/notes.txt b/2020-frama-c/notes.txt
index b7254f7..7cb905c 100644
--- 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]
+
 
 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.
 
 
+= 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.
+
+
 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.
 
 
-= 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.
-
-
-= BACK TO RANGE.C =
-
 Going back to what we proved so far:
 
   /*@