From bb6d169e8983d33850dc99a9704242ed06cc159b Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Wed, 14 Oct 2020 12:42:22 +0100 Subject: [PATCH] Add outline of slides. --- 2020-frama-c/.gitignore | 2 + 2020-frama-c/1000-introduction.html | 21 +++++++ 2020-frama-c/bashrc | 22 ++++++++ 2020-frama-c/code.js | 0 2020-frama-c/functions | 46 ++++++++++++++++ 2020-frama-c/redhat.png | Bin 0 -> 8766 bytes 2020-frama-c/restore | 3 + 2020-frama-c/run | 23 ++++++++ 2020-frama-c/style.css | 107 ++++++++++++++++++++++++++++++++++++ 9 files changed, 224 insertions(+) create mode 100644 2020-frama-c/.gitignore create mode 100644 2020-frama-c/1000-introduction.html create mode 100644 2020-frama-c/bashrc create mode 100644 2020-frama-c/code.js create mode 100644 2020-frama-c/functions create mode 100644 2020-frama-c/redhat.png create mode 100755 2020-frama-c/restore create mode 100755 2020-frama-c/run create mode 100644 2020-frama-c/style.css 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 0000000000000000000000000000000000000000..c955eb021fe842672e0fbb454f780f82fd12b0e7 GIT binary patch literal 8766 zcmV-EBEj8>P)O002J-1^@s6%3F*(000rjdQ@0+Qek%> zaB^>EX>4U6ba`-PAZ2)IW&i+q+O3&sl3h7&M*njaUIIZ99G1fg5#B*B-v@lJq?StE z4m(;|mBY}Fed!PQjk^H#v` z{mf1`yPw_7QUm3x-%b6s#rGX2F3OqTWtES{|H}96eGEQ&oN?2&!&X;_iyww0s%cW> z$P|A1=<%-~;r9do-;ZBzWaeWo;>D!(@@a7L`C=K~IseRAG(_xMQ+@T7@c9yd|L2X( zbWmTJI~$yFeQvQ-e$G~Yea=w>rQnXa?))}E0G;2}Ss!h8N zoi*1|wbt6I^VDp)m8Pw>)_NOl_S{R?UVH1kk3L5l85+|t>S&{nG3Mlu$U6vFAxAA1EN4dfMq{oO$IkO1E6S^|ssZxYL+5%T`RS zTC;A$=8vv@yZUR_e(&7B@0xtOmR_U$y!Nwe9B%EeTZq$%de7)sDniGbcYuLT-m}=H zl;oZBp2d-J$XOGsRBz4^?-(5{SCX3i=-toG{mZ@us{4QKTl!Pyg17EJ(YfHQ`=`$R zy>EZ$+L@1T^J|c!keb4fu56q%Q|CW;XN|!l>X|xjaYCwm*N0JZ%lpn{5^0~bG0z@t zapuq+ba8Ck(75YCwANuWC)&+=XEUL4!|q-ddp>Idq`FSEr0}HmHdni2x0?e`vD3!r zXYK=NAVTAp()OBczwag9(s2xNzvr-YOL?uetuIDc);>w+4!aGBd){1^?gEYH%ad8s zIxXi(rv{Zisq)0MmzFhqzbzHoqjbueLS4;*%uTOWpA0}_BqnQrVqZJUUg-7}}-A!p6d(uX`^^CT2 zIy%eAZ8LQ%h%d1U)lft6)pKr>H7*` zm~_f9^BtqHJVs(%)yaHGXakr7j+yCs)b%>ZX4-aE@Xa+y=%DWXT9ZsMSdEH5!rWIX#D9C@B6b6^ z^s_|y^b{VYo3c;dls$4~-gD5q#b5CKv}cWqG5kj$Pt zlSZ>**6NL*Wz*Vf!C9c`TxXxNH`aqQ)4mt_2H-k7TL25w%T1-=x49N8jd-l0OfI0O zl{wh1bL|B}4mUVD2Gg~HH)WR589Wff0{2L3U#36tj6p*hMyj?!YaL+{1meAvYgHS| zpJ^#s>y|Gf;LzW?fD!kF1YFVuRe=g5Jk`SV%Uw#?ZBawyoXFwdAJL zN^wwS+uZ1K*}pEfwG4XHBc zJI;fXQ?o2u0sZey9_mX9%=bU{}+T^LOHR#6>3FyH97dq^Kr*4=Cz~&2TGjyi8_g&D#a~tr%-QB(s z-V70``EUt{%Gt&mj?4@hBjzr0LO}{C2TP7U0&&xy+bCjj-6hxE}Wd8!5wPZ#%$Ih*wy^ zg93mP`WIOjpzNtta}^HA4#c?OE5SY58W=tHLO`!@DuRpi(#qVu_=w+Kz^rot9*{<- zxCUfUdO*Oq9x`Bnfd=-N!sE>6UBGsN`0jMyQWJ_p zE?HPjD$3|E?O^+QkSIWo$-po3JPb0cvjD0SQa~Cco464pHDMgvQ+gBUrZp$Jg6BVk z%;V^F9}my5COUangen8!r7ZeYZ^v|&3(Baj+cF|>&aom5MB&ZwLM}YW?KH00by8A4 zv2Ty_DH!1#9HmC&xYzTZ-w2`Fq?-oCUIjS&?hz)ig{xxKun}3>>R><{xDs6fVb!1KxV4DI4X zoDpsp)kYPuaUEA)UCYse<-Vt?2keA^C;beHAn5qXlXsPVZP*%{xigv%g@uyziB zZHq+mmTnExy*ztWNECWD*OUl|R)I&%;ev9qP38-ji@&iLP|k3fH$g@rGIzv*q@IPL zLz0Nt7_IIvsnME(f5F${_1Vou7N8+?T*1!4hn}I#((-pDu51F<$j*!kRD$6=+jSob zsLU@DQ_w^Fb}G0Iu$myZkv5IR8*zK)9!JDQ3?vxFKp^B!IAqEJ(OlHt4LQ?J`!TiK zC9!dVE-)<+&Sgmjvx(A@{ZJKurI8Qq_?xf$;p#l_VrbmVA^n`vJ@XXk7=%MR{rIbx zFfnoDQrbmGCN2})J3qDU?Z{N&ycZYPA_hlt8RoX8-d18UMn=vvQW7H9h)`D??F6+G zvn?1hg5aG^h!zd!N@~Cf+-FPs+H$Zi|unqyz?P~S+127d9rIa19z0uu1^T+;q&SrFYnquKzWGDT= zzSsR{=oS2>=`T_It%Az4MwoTCMl(70kj#gd4$C)4dQ?5)WbkJR@i|WRxCflSmjEOp z!Jb!O`= zJ^qpszQ>CovS-|elfruY<#0O;K;y88n6FTYdRPZSboAKG7B)}Bv=JBR=Z);(_=_uu zz6heHZd``H5NQ5N%)J6hksIN{CW=L{9!M4ZOIEl<%CW_*aCJX1DEJh2A&>#1K|)E%&1m&ZN`Kzpy|4nscLz)TVg?kNe#mSy5-F__JhQr&zGY2 z0-GywoSfr-AcCPA+#*mK%O-hKKJLQ!!@DwSsDg$d;+y&Rzr`T{%gt5xSFG+z9r}}y zKi~V=jJNbVI3O5_mbSkmDm4Zer1_4HRAvH?g!{z7El9rmTfW4UAhzgYamUi)U4YvE zZgQ@p3?G}AN(&xbfsX6YTBo6XiEs~bSIXP4A7pe$s;lB3JFHiz6!k4H6#zdee|3fB2pU^R#?#?5+25l;;Lok9p z)Q1{@z|>1e7X58Alt%A8fYDQ=g_SV9C=C7|7W2QJWjH(I@MnkAH#NZ~&<3zLoCAde z*mfh$d8}jjDh0vKp>c^`c34kb@YkKe;4ISXSO5>-2qd+m1%_-0*vbqIv}S3%HxvvQ z^&QyeYB(4&E|TGY2(&QBm6J~&ohRtKyG1VPKKjax5PB2N-)(tCphqGmOjg3T8FfP^ zC?F64Po6kIc6H@N<=Goh0+y&8)dnDSl&kb9QGip9+l=_$C#n}6nj#hj1_eaRBt9+# zCVk#QV-X#w%t-UWO0{BFNk4six%|&9h4jR<5E%=`)3qNSEEre-iD`(W-pY6brg^u& zI)85z+`~`jeK(Vhd!u&j4X2heH{_8eOlWc(zZJ2@0Q;?&1t6lZ!h1Uo)(BJ7|LA*9 zvu0hLL=fM~pQ9sd2Z$jN!95cCdwz2Uc7`}^*{~j}pZ7`d)H7b_u-i}jzGeF4BVyru zF-{LDha+VmK?^4*{FFH6;-2rf7WG%^A=~dQe&-q@)w5l z+R8H5X^tR?MJz#t02wuuQGtaRtr{sN(zKuO@DDqFkz6vl%3$PJKou$^#}EDozq>UH zQ4lRq6&fI0VLul)dip?w-!x{yo#` z?+47;a?4G@A6)^H|_G%tWK)ZW9npBDtLFI?T^MAKOG1vRN$h zJZ_{?mWB~Ziy0H>uA-lfy{z;Un)gM1SR2*OA%4Mhp;0yGK*9Hvq@(=_sJARq{n zTVxpqj94uA3qeu%R8>j9mw+HFmdiU@g6rvMaS0zbOi%|C3idt!! z_WU`zu0z-LuD?$t5=bNxzTU&2-WN^N5RFEAo^MB3L&EX)wsio6@;Kh!w#EsXrY!)z z9m!y8i9`a@m}|TUf`LRLfmket_4Rd#qKHzd1k+~~ z{ZPoI^2;yKLh2IPZqX#dG)-)7Zh|8XwWc0>9(p4Ml3cd8wm^k=;Vsj|xq}ZLb`%N) zLNEm3B$t2w{4<_YRHzqb(o@ofLIHA!T~~rBBo|qhVVWkkOcTF`cwtVaAdShBatDGT zqOVl6Wf(ZqG@NM~&YS z1VMo4(z94qRabJ+G!3#Ww@Ay*Do_-KR4Rp3Dg}0rELfK9s+$o6p{KD`RqgsW9LITId$(Nm zQ7&g0@wg{_$jdG{{WXfRN+Hy{GG>jQVHpFy5~0~&+|y9(;eT=PGe09 zR8>VHkw7|~MxjvXOK)PDCPYyL!!W+7yN43cJ<~M2W0-+S<;vvib^Q702wNe_B27aP zWBV7;FbpsZgBJr-vx}nWDUM?p22!aMc6N5AK0e`>?xb8Udvck_LN4~shW+%sy$67b zL>$lAGELAcE1}3FsT1&aR9sp}wENEt!=UVg0J2ahxLPnQ%la}_*ugMNPqk292&Px- zaU|q&#Pb6+)4sp7&2q2RKi+~puF&-1=M?4l^P0({TZ{EgdK0IW=j>R= zF)sgbQY`xRU_Mx0?rYI)lBooMT-GScqHf)?j&eEce1z=^Mnx|6Ltm@a26|9ywVLC@ zzOk`!<$O0{=tgAiV@?{mSeA8-h@G&zyW2NOjDlQ-)-3AD!2z(mjAsW2J^kGq)5Kqz zf#Lg0OZaYoA9u%Krv7z#8E=}`{y$MfT$1n!&tsA2Ct_3kd_Lcbx45}jwmI$uj^nzz zRf?jtT0N+$>S)f>H0>!~FsTi&dJ!VpE^SaTH_Q+3mtcU4)b+D^9nS!)#bUUB;|Bgz zt&W6f{@QlUzXDh@O&p6NK1vd9$ui~xeq+0Vq9{m`bR|`+x#)RBQS=-m>E{1?4Um(1 zr;8N5qA0BxQzv4zmC>OgmtkxO_T=CI)XEBes#g2{j5oC!egg1QlW6YUzKt)dReV{m zW6j5FeIAKmYhj^fvDo-;JdXR#2gEW>ykB3(LN<$=k`yW{#F>;t#bND8SXiF`E|2e_}Dbx_uk3s@02Y^LTxYLIG!*hTDpQ*^tz^2!hZt z3!nu=i5!o|1G#S5Y_{j(&R)~{vMht=`H9MeU2}^Tc^)4gKJMR&A*kVqtYmLv2M6Vfyd4~Ou~jT_fQbPF7Z*&)3_)&RVyR`E0v0kya|(uuwq z;Ek|!c-ZxKmTBT0!;G{=Ln@U5!!XwlHzC&E-d@LGX^<+6wJF^3a#G_=9Rs>IB?<4> z*M~OfxAi*y2;d(B#$rZ=uU#w~%QW$xWwE4bV~xRZ90x%V94!Ez=dYFLy9EX}HZ}&1 zh1g@bjU@v{WAJ&UoU{sQ% zD;c6_G>S|n(><YZgmY)xf7={cr=vRd%8% ziZ2<&t~!^QXcV^DCX>0+2~O8_sH)mZpKfk$woG;>0(48a?(FPfXJ-eQ zOr}L7_E>>-1^RRsyFKLH;xU)I^!W|bG+W&TFOO&MZaJ`9bh+NBMp0vt-)n&NV=QLf zU0E5aEA;)!%0T4@A3d1$!|p`qrG%ipc4cE@!?!ieX0whvJo-6SnBAgErQ&#AJRY}l zxtvuj7Oi5jXytM_&)w>ruG_6HsoUY}j*B;%sn(e>G;;QN&oXt>bj3^LnB00NR;O8DEg8-gGpnN0dJexXos?26{+SYbvYk#Jmx zy}dn%qKI@ljdVHdw1^O(dsH*0;tsMcwDXeqWBF$2Rknfh)Si>l{iW?8ilH=zCHBia=B{^ z#_zGhjB#wSJBswT=Y5N8g1HfpF9U^(&UfF{YWVxxw|KF)2d!4a0e}MlT9bU*53Tw8 zO1+MkZ{On4{yy&cd~HG5vC)h5(teKp&^rZqy&{*(IbMT3mY-eN!U%?8u(7c*a*HXS z&j*8CE)&eW4_~}dxK#H#9BU&QKM3UF)p}_UzDA=_D2jsJ-QB(<`7}+VQmJ?%H=AJc z`Ml?`D2hTZmzy~2C7;iO>cKl0l$1G+>v_yx&~sI^okjX6NjTcv1cCo>OSASOEf)mA z^&#)Jcagmxj-n{7y@a}DYG|4U!!W(=Yt!~c=Qyr4mZoV}YIE#8l311n$8jxE>URy> z-{MXWYCrSo=N@t#2bN_a%Q6&2>AF{uz0S5$dywn4$Gp7m?f00b=~gGap17hZsObx5 znuZS?=X;^!Bp_O=O+??9PS7;16{rnb3s8dKU?6g_Q5OV!l%$d9VZwsg;LA!t5Ni0c z5q(4uu%v02oASV1%hx39KtSLRxd6ayB7sj;6`vN1BPkmQG8U$|;Sm9WuWnH%G-Mfd zLGX3g#!xIMMS;@wiH)}q5RBY%x%T$vI8eHdTlxG{Su&qYNCR&Ig1}lX(`d=e#^Yn} z=|Vs-b>w2>L{V@oNjRN=eVE(bp;5QHBp@K<(gEkXj$=teLzX8Zg?%fZ$3l-yoCydB zxs1S?X($RB9=22nqQ!DsQ7}iuWCR4kBNrQ%VYGePn0j)#jB{PbsjA{cRdK4SV