From d7e556c576cedd722ff0115cec75e6dc09ce1da2 Mon Sep 17 00:00:00 2001
From: "Richard W.M. Jones" <rjones@redhat.com>
Date: Mon, 16 Nov 2020 12:20:51 +0000
Subject: [PATCH 1/1] Tighten intro.

---
 2020-frama-c/1500-frama-c-core-plugins.html | 14 ++++++++++++--
 2020-frama-c/1600-frama-c-plugins.html      | 12 ------------
 2 files changed, 12 insertions(+), 14 deletions(-)
 delete mode 100755 2020-frama-c/1600-frama-c-plugins.html

diff --git a/2020-frama-c/1500-frama-c-core-plugins.html b/2020-frama-c/1500-frama-c-core-plugins.html
index e891690..fd3cb3b 100755
--- a/2020-frama-c/1500-frama-c-core-plugins.html
+++ b/2020-frama-c/1500-frama-c-core-plugins.html
@@ -10,12 +10,22 @@ Frama-C &mdash; Framework for Static Analysis of the C language
 
 <h2>Core</h2>
 
-<p>
+<ul>
+<li>
 C source code &rarr; Abstract Syntax Tree
-</p>
+<li>
+ACSL &mdash; ANSI/ISO C Specification Language <br>
+<code>/*@ ... */</code>
+</ul>
 
 <h2>Plugins</h2>
 
 <p>
 Annotate syntax trees with static analysis.
 </p>
+
+<ul>
+<li> WP &mdash; <a href="http://www.cs.umd.edu/~mvz/handouts/weakest-precondition.pdf">Weakest Precondition</a>
+<li> Value analysis, Jessie, InOut, Metrics, Aorai, PathCrawler, Spare code, ...
+<li> several in-house plugins at Atos, Airbus, Dassault, CEA, ...
+</ul>
diff --git a/2020-frama-c/1600-frama-c-plugins.html b/2020-frama-c/1600-frama-c-plugins.html
deleted file mode 100755
index 8e52e20..0000000
--- a/2020-frama-c/1600-frama-c-plugins.html
+++ /dev/null
@@ -1,12 +0,0 @@
-<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>
-- 
1.8.3.1