Slides for 3xxx.

diff --git a/2020-frama-c/2300-range-is-empty.term b/2020-frama-c/2300-range-is-empty.term
index 09c6e27..02d88c4 100755 (executable)
--- a/2020-frama-c/2300-range-is-empty.term
+++ b/2020-frama-c/2300-range-is-empty.term
@@ -3,7 +3,7 @@
 source functions
 
 # Title.
-export title="qemu"
+export title="qemu’s range_is_empty()"
 
 # History.
 remember 'cat snippets/range_is_empty.c'

diff --git a/2020-frama-c/3000-frama-c.html b/2020-frama-c/3000-frama-c.html
new file mode 100755 (executable)
index 0000000..e891690
--- /dev/null
+++ b/2020-frama-c/3000-frama-c.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>
+
+<h1>Frama-C</h1>
+
+<p>
+Frama-C &mdash; Framework for Static Analysis of the C language
+</p>
+
+<h2>Core</h2>
+
+<p>
+C source code &rarr; Abstract Syntax Tree
+</p>
+
+<h2>Plugins</h2>
+
+<p>
+Annotate syntax trees with static analysis.
+</p>

diff --git a/2020-frama-c/3100-frama-c.html b/2020-frama-c/3100-frama-c.html
new file mode 100755 (executable)
index 0000000..8e52e20
--- /dev/null
+++ b/2020-frama-c/3100-frama-c.html
@@ -0,0 +1,12 @@
+<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>
+
+<h1>Frama-C</h1>
+
+<img src="slides/slide01.png" height="75%" />
+
+<p class="attribution">
+Slides from
+<a href="https://www.cs.umd.edu/class/spring2016/cmsc838G/frama-c/introduction-to-frama-c_v2.pdf">David Mentré’s 2016 introduction to Frama-C</a>.
+</p>

diff --git a/2020-frama-c/3200-frama-c.html b/2020-frama-c/3200-frama-c.html
new file mode 100755 (executable)
index 0000000..306c037
--- /dev/null
+++ b/2020-frama-c/3200-frama-c.html
@@ -0,0 +1,12 @@
+<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>
+
+<h1>Frama-C</h1>
+
+<img src="slides/slide02.png" height="75%" />
+
+<p class="attribution">
+Slides from
+<a href="https://www.cs.umd.edu/class/spring2016/cmsc838G/frama-c/introduction-to-frama-c_v2.pdf">David Mentré’s 2016 introduction to Frama-C</a>.
+</p>

diff --git a/2020-frama-c/3300-frama-c.html b/2020-frama-c/3300-frama-c.html
new file mode 100755 (executable)
index 0000000..1825037
--- /dev/null
+++ b/2020-frama-c/3300-frama-c.html
@@ -0,0 +1,12 @@
+<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>
+
+<h1>Frama-C</h1>
+
+<img src="slides/slide03.png" height="75%" />
+
+<p class="attribution">
+Slides from
+<a href="https://www.cs.umd.edu/class/spring2016/cmsc838G/frama-c/introduction-to-frama-c_v2.pdf">David Mentré’s 2016 introduction to Frama-C</a>.
+</p>

diff --git a/2020-frama-c/3400-frama-c.html b/2020-frama-c/3400-frama-c.html
new file mode 100755 (executable)
index 0000000..d718096
--- /dev/null
+++ b/2020-frama-c/3400-frama-c.html
@@ -0,0 +1,12 @@
+<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>
+
+<h1>Frama-C</h1>
+
+<img src="slides/slide04.png" height="75%" />
+
+<p class="attribution">
+Slides from
+<a href="https://www.cs.umd.edu/class/spring2016/cmsc838G/frama-c/introduction-to-frama-c_v2.pdf">David Mentré’s 2016 introduction to Frama-C</a>.
+</p>

diff --git a/2020-frama-c/3500-frama-c.html b/2020-frama-c/3500-frama-c.html
new file mode 100755 (executable)
index 0000000..553d9de
--- /dev/null
+++ b/2020-frama-c/3500-frama-c.html
@@ -0,0 +1,12 @@
+<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>
+
+<h1>Frama-C</h1>
+
+<img src="slides/slide05.png" height="75%" />
+
+<p class="attribution">
+Slides from
+<a href="https://www.cs.umd.edu/class/spring2016/cmsc838G/frama-c/introduction-to-frama-c_v2.pdf">David Mentré’s 2016 introduction to Frama-C</a>.
+</p>

diff --git a/2020-frama-c/notes.txt b/2020-frama-c/notes.txt
index 733cba8..d41e161 100644 (file)
--- a/2020-frama-c/notes.txt
+++ b/2020-frama-c/notes.txt
@@ -94,18 +94,16 @@ checked it, and it's correct - the code is bug-free.
 \f
 = OVERVIEW OF FRAMA-C ECOSYSTEM =
 
+Let's interrupt this and talk about Frama-C.  The name stands
+for "Framework for Static Analysis of the C language".
 
-XXX Modular Framework for analysis of C
-
-XXX Take some slides from David Mentre's presentation.
-
-XXX Explain which companies are using Frama-C.
-
-XXX WP plugin
-
-XXX ACSL language
-
+It's modular, with a core program that reads C source code
+and turns it into Abstract Syntax Trees.  And a set of plugins
+to do static analysis by annotating these syntax trees.
+Plugins can cooperate, so analysis can be passed between
+plugins.
 
+The following slides are taken from David Mentré‘s 2016 presentation.
 
 \f
 = BACK TO RANGE.C =

diff --git a/2020-frama-c/slides/README.txt b/2020-frama-c/slides/README.txt
new file mode 100644 (file)
index 0000000..c851fd1
--- /dev/null
+++ b/2020-frama-c/slides/README.txt
@@ -0,0 +1,2 @@
+These slides taken from David Mentré's presentation:
+https://www.cs.umd.edu/class/spring2016/cmsc838G/frama-c/introduction-to-frama-c_v2.pdf

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

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

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

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

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