From: Richard W.M. Jones Date: Wed, 14 Oct 2020 11:42:22 +0000 (+0100) Subject: Add outline of slides. X-Git-Url: http://git.annexia.org/?p=libguestfs-talks.git;a=commitdiff_plain;h=bb6d169e8983d33850dc99a9704242ed06cc159b Add outline of slides. --- diff --git a/2020-frama-c/.gitignore b/2020-frama-c/.gitignore new file mode 100644 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 index 0000000..991dc59 --- /dev/null +++ b/2020-frama-c/1000-introduction.html @@ -0,0 +1,21 @@ + + + + +
+

+ Formally proving tiny bits of qemu using Frama-C +

+ +

+ Richard W.M. Jones (rjones @ redhat.com)
+ Monday November 16th, 2020 +

+ +

+ Formal verification of software proves that the software is + mathematically correct with respect to its specification. + Frama-C is an open source modular framework for formal verification + of programs written in C. +

+
diff --git a/2020-frama-c/bashrc b/2020-frama-c/bashrc new file mode 100644 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 index 0000000..e69de29 diff --git a/2020-frama-c/functions b/2020-frama-c/functions new file mode 100644 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 +# +# 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 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 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 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 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; +}