Slides for 2xxx.

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

diff --git a/2020-frama-c/notes.txt b/2020-frama-c/notes.txt
index 4b15f26..733cba8 100644 (file)
--- a/2020-frama-c/notes.txt
+++ b/2020-frama-c/notes.txt
@@ -70,7 +70,7 @@ Notice a few things here:
 
  - I'm using structs directly from the C code.
 
- - The comments in the upstream code translate into predicates.
+ - The upstream comments translate into machine-checkable code.
 
 The first upstream function is:
 
@@ -82,7 +82,7 @@ The first upstream function is:
 
 and using the predicates we can write a specification:
 
-  $ less snippets/range_is_empty.c
+  $ cat snippets/range_is_empty.c
 
 And we can compile and prove that: