Add outline of slides.

diff --git a/2020-frama-c/.gitignore b/2020-frama-c/.gitignore
new file mode 100644 (file)
index 0000000..d678620
--- /dev/null
+++ b/2020-frama-c/.gitignore
@@ -0,0 +1,2 @@
+/bindings
+/history

diff --git a/2020-frama-c/1000-introduction.html b/2020-frama-c/1000-introduction.html
new file mode 100644 (file)
index 0000000..991dc59
--- /dev/null
+++ b/2020-frama-c/1000-introduction.html
@@ -0,0 +1,21 @@
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
+<link rel="stylesheet" href="style.css" type="text/css"/>
+<script src="code.js" type="text/javascript"></script>
+
+<div id="titlepage">
+  <p class="title">
+    Formally proving tiny bits of qemu using Frama-C
+  </p>
+
+  <p class="author">
+    Richard W.M. Jones <small>(rjones @ redhat.com)</small> <br/>
+    <small>Monday November 16th, 2020</small>
+  </p>
+
+  <p class="abstract">
+    <b>Formal verification</b> of software proves that the software is
+    mathematically correct with respect to its specification.
+    <b>Frama-C</b> is an open source modular framework for formal verification
+    of programs written in C.
+  </p>
+</div>

diff --git a/2020-frama-c/bashrc b/2020-frama-c/bashrc
new file mode 100644 (file)
index 0000000..0b5a00c
--- /dev/null
+++ b/2020-frama-c/bashrc
@@ -0,0 +1,22 @@
+# -*- shell-script -*-
+
+# Colour ls.
+if [ -f /etc/profile.d/colorls.sh ]; then . /etc/profile.d/colorls.sh; fi
+
+# Fancy prompt colours (see
+# https://wiki.archlinux.org/index.php/Color_Bash_Prompt)
+titlecol=$'\e[1;37;41m'    ;# colour for the title
+promptcol=$'\e[0;32m'      ;# colour for the prompt
+commandcol=$'\e[1;31m'     ;# colour for the typed command
+outputcol=$'\e[0m'         ;# colour for command output
+
+export PS1="\n\[$promptcol\]\$ \[$commandcol\]"
+
+trap 'echo -ne "$outputcol"' DEBUG
+
+# Load key bindings (if any).
+bind -f $talkdir/bindings
+
+# Same as the banner function, but we cannot reuse it.
+printf "\e]0;$title\a"
+printf "%s   %s   %s\\n" $titlecol "$title" $outputcol

diff --git a/2020-frama-c/code.js b/2020-frama-c/code.js
new file mode 100644 (file)
index 0000000..e69de29

diff --git a/2020-frama-c/functions b/2020-frama-c/functions
new file mode 100644 (file)
index 0000000..94948e2
--- /dev/null
+++ b/2020-frama-c/functions
@@ -0,0 +1,46 @@
+# -*- shell-script -*-
+# This creates some standard functions.  See also $talkdir/bashrc
+# which runs in the same bash context as the terminal.
+
+# Place any local environment variables and settings in "local".
+if [ -f local ]; then source local; fi
+
+# Environment variables.
+export HISTFILE=$talkdir/history
+export PATH=$talkdir:$PATH
+export EDITOR="emacs -nw"
+
+# remember <command> <args ...>
+#
+# This function does two things: (1) It adds the command and arguments
+# to the shell history, so that commands can be recalled using up
+# arrow or reverse search.  (2) It makes a function key recall the
+# command.  The first command is assigned to F2, the second to F3 and
+# so forth.
+
+rm -f $HISTFILE
+touch $HISTFILE
+rm -f $talkdir/bindings
+touch bindings
+
+fnum=2
+keys=(- OP OQ OR OS '[15~' '[17~' '[18~' '[19~' '[20~' '[21~')
+
+remember ()
+{
+    echo "$@" >> $HISTFILE
+    echo "$@" | sed -e 's/"/\\"/g; s/$/"/' \
+        -e 's/^/"\\e'"${keys[$fnum]}"'":"\\C-k \\C-u/' >> $talkdir/bindings
+    ((fnum++))
+}
+
+terminal ()
+{
+    chmod -w $HISTFILE
+    /bin/bash --rcfile $talkdir/bashrc "$@"
+}
+
+banner ()
+{
+    printf "%s   %s   %s\\n" $'\e[1;37;41m' "$1" $'\e[0m'
+}

diff --git a/2020-frama-c/redhat.png b/2020-frama-c/redhat.png
new file mode 100644 (file)
index 0000000..c955eb0
Binary files /dev/null and b/2020-frama-c/redhat.png differ

diff --git a/2020-frama-c/restore b/2020-frama-c/restore
new file mode 100755 (executable)
index 0000000..00bc41f
--- /dev/null
+++ b/2020-frama-c/restore
@@ -0,0 +1,3 @@
+#!/bin/bash -
+
+# (nothing)

diff --git a/2020-frama-c/run b/2020-frama-c/run
new file mode 100755 (executable)
index 0000000..d6333b0
--- /dev/null
+++ b/2020-frama-c/run
@@ -0,0 +1,23 @@
+#!/bin/bash -
+# Run the talk.
+
+set -e
+
+# Avoid GNOME keyring stupidity
+export GNOME_KEYRING_CONTROL=
+export GNOME_KEYRING_PID=
+
+# No proxy.
+#unset http_proxy
+#unset https_proxy
+#unset ftp_proxy
+
+# Clean up after previous run.
+talkdir=$PWD ./restore
+
+# Precreate any files necessary.
+#(nothing)
+
+# Run techtalk.
+techtalk-pse
+#~/d/techtalk-pse/techtalk-pse

diff --git a/2020-frama-c/style.css b/2020-frama-c/style.css
new file mode 100644 (file)
index 0000000..093a8b7
--- /dev/null
+++ b/2020-frama-c/style.css
@@ -0,0 +1,107 @@
+/* Red Hat red is rgb(238,0,0). */
+
+body {
+    background: url(redhat.png) no-repeat;
+    background-position: 98% 6px;
+    background-size: auto 48px;
+    /* font-size: 28pt; */ /* For max */
+    font-size: 20pt; /* For 1024x768 */
+    font-family: Red Hat Text, liberation, helvetica;
+    /* font-family: helvetica; */
+
+    /* Can be used to scale the whole document. */
+    /*transform: translate(-10%,-10%) scale(0.75,0.75);*/
+}
+
+body td, body th { /* why?? */
+    font-size: 24pt;
+    padding-bottom: 8px;
+}
+
+h1 {
+    color: rgb(238,0,0);
+    /*font-size: 48px;*/
+    font-size: 40px;
+    top: 8;
+    left: 0;
+    border-bottom: 2px solid rgb(238,0,0);
+}
+
+h2 {
+    color: rgb(238,0,0);
+    font-size: 32px;
+    font-style: italic;
+    border-bottom: 2px solid rgb(238,0,0);
+}
+
+b {
+    color: rgb(238,0,0);
+}
+
+/* Title page. */
+div#titlepage {
+    margin-top: 100px;
+    width: 80%;
+    margin-left: 10%;
+}
+
+div#titlepage p.title {
+    color: rgb(238,0,0);
+    font-weight: bold;
+    font-size: 48px;
+    text-align: left;
+}
+
+div#titlepage p.author {
+    font-size: 36px;
+    text-align: left;
+}
+
+div#titlepage p.abstract {
+    font-size: 28px;
+    text-align: left;
+}
+
+/* Code */
+pre.code {
+    margin-left: 1em;
+    background: #eee;
+}
+
+code {
+    color: rgb(238,0,0);
+}
+
+/* Bullet points */
+li {
+    padding-bottom: 16px;
+}
+
+/* For images which must be centered on the page. */
+div.allcenter {
+    display: flex;
+    justify-content: center;
+    align-items: center;
+    height: 50vw;
+}
+
+div.all-center img {
+}
+
+/* Attribution for artwork etc. */
+p.attribution {
+    position: absolute;
+    right: 10px;
+    bottom: 10px;
+    text-align: right;
+    font-size: 10pt;
+}
+
+/* Tables */
+table#border {
+    border-collapse: collapse;
+}
+
+table#border th, table#border td {
+    border: 1px solid black;
+}