Add page breaks in notes.

[libguestfs-talks.git] / 2020-frama-c / notes.txt

diff --git a/2020-frama-c/notes.txt b/2020-frama-c/notes.txt
index afe5f1c..4b15f26 100644 (file)
--- 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 will provide links to tutorials etc at the end.
 

+\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:
 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.
 
 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 =
 
 
 = OVERVIEW OF FRAMA-C ECOSYSTEM =
 
 


@@ -105,6 +107,7 @@ XXX ACSL language
 
 
 
 
 
 

+\f

 = BACK TO RANGE.C =
 
 Going back to what we proved so far:
 = 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.
 
  - Given those assumptions, the code is bug free - you don't need to
    write any tests.
 

+\f

 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:
 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;
   }
 
       return val >= range->lob && val <= range->upb;
   }
 

+\f

 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:
 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));
   }
 
       assert(range_is_empty(range));
   }
 

+\f

 I'm going to skip forward a few functions to get to an interesting one.
 This seems trivial:
 
 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
 
 
   $ frama-c -wp -wp-rte snippets/range_size-good.c
 

+\f

 On to the next function.  Again this seems very simple, but in fact it
 contains a serious problem:
 
 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.
 
  - It probably doesn't make sense for qemu right now though, unless we
    could prove more substantial pieces of code.
 

+\f

 = POWER OF 2 =
 
 This is a function from nbdkit:
 = 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.
 
 Essentially bitwise tricks like this are a hard case for automated
 theorem proving.  I gave up.
 

+\f

 = TIMEVAL DIFFERENCE =
 
 This is another nbdkit function:
 = 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.
 
    understand them.  We could contribute these to the Frama-C standard
    library.
 

+\f

 = STRING FUNCTIONS =
 
 Uli sent me this function from glibc:
 = STRING FUNCTIONS =
 
 Uli sent me this function from glibc:


@@ -589,6 +599,7 @@ documented.
 
 So a proof of the glibc function eludes me.
 
 
 So a proof of the glibc function eludes me.
 

+\f

 There is a set of open source licensed string functions with Frama-C
 proofs available:
 
 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:
 
 
 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]

 
 

+\f

 Now you might be asking what happens when you write a function that
 uses strlen, for example this trivial function with a working
 specification:
 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!
 
 strings cannot exist on real computers, but they can exist on
 theoretical ones!
 

+\f

 = IN CONCLUSION =
 
 * Frama-C is a real open source tool used by companies to verify
 = IN CONCLUSION =
 
 * Frama-C is a real open source tool used by companies to verify