Tighten intro.

[libguestfs-talks.git] / 2020-frama-c / 1500-frama-c-core-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 (executable)
--- 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 — 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>