From: Richard W.M. Jones <rjones@redhat.com>
Date: Wed, 14 Oct 2020 11:27:08 +0000 (+0100)
Subject: Add page breaks in notes.
X-Git-Url: http://git.annexia.org/?a=commitdiff_plain;h=e17fe3e420e90cf5aa5ab2212b8825a27ff455c5;p=libguestfs-talks.git

Add page breaks in notes.
---

diff --git a/2020-frama-c/notes.txt b/2020-frama-c/notes.txt
index afe5f1c..4b15f26 100644
--- a/2020-frama-c/notes.txt
+++ b/2020-frama-c/notes.txt
@@ -13,6 +13,7 @@ tool.
 
 I will provide links to tutorials etc at the end.
 
+
 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:
@@ -90,6 +91,7 @@ And we can compile and prove that:
 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 =
 
 
@@ -105,6 +107,7 @@ XXX ACSL language
 
 
 
+
 = BACK TO RANGE.C =
 
 Going back to what we proved so far:
@@ -153,6 +156,7 @@ We need to be very clear about what happened:
  - Given those assumptions, the code is bug free - you don't need to
    write any tests.
 
+
 Obviously this is a single line, very trivial function, but I was
 quite pleased that I was able to prove it quickly.  I kept going on
 the range file.  The next function is:
@@ -183,6 +187,7 @@ top of the file:
       return val >= range->lob && val <= range->upb;
   }
 
+
 The next function is range_make_empty, again easy to prove using the
 already existing empty_range predicate.  Notice how we declare which
 memory locations this function assigns to:
@@ -200,6 +205,7 @@ memory locations this function assigns to:
       assert(range_is_empty(range));
   }
 
+
 I'm going to skip forward a few functions to get to an interesting one.
 This seems trivial:
 
@@ -314,6 +320,7 @@ that callers do not try to call range_size() on the empty range.
 
   $ frama-c -wp -wp-rte snippets/range_size-good.c
 
+
 On to the next function.  Again this seems very simple, but in fact it
 contains a serious problem:
 
@@ -398,6 +405,7 @@ point out a few things about the final proof:
  - It probably doesn't make sense for qemu right now though, unless we
    could prove more substantial pieces of code.
 
+
 = POWER OF 2 =
 
 This is a function from nbdkit:
@@ -449,6 +457,7 @@ about Alt-Ergo (the default prover):
 Essentially bitwise tricks like this are a hard case for automated
 theorem proving.  I gave up.
 
+
 = TIMEVAL DIFFERENCE =
 
 This is another nbdkit function:
@@ -539,6 +548,7 @@ A few things I learned from this:
    understand them.  We could contribute these to the Frama-C standard
    library.
 
+
 = STRING FUNCTIONS =
 
 Uli sent me this function from glibc:
@@ -589,6 +599,7 @@ documented.
 
 So a proof of the glibc function eludes me.
 
+
 There is a set of open source licensed string functions with Frama-C
 proofs available:
 
@@ -596,8 +607,9 @@ https://github.com/evdenis/verker
 
 and this is what the strlen function with proof looks like from that:
 
-  [https://github.com/evdenis/verker/blob/master/src/strlen.c
+  [https://github.com/evdenis/verker/blob/master/src/strlen.c]
 
+
 Now you might be asking what happens when you write a function that
 uses strlen, for example this trivial function with a working
 specification:
@@ -630,6 +642,7 @@ which is used to represent an unbounded string.  Of course unbounded
 strings cannot exist on real computers, but they can exist on
 theoretical ones!
 
+
 = IN CONCLUSION =
 
 * Frama-C is a real open source tool used by companies to verify