X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=2020-frama-c%2F1500-frama-c-core-plugins.html;h=fd3cb3b82e884159a68214b2fd01adf8b5ae9d23;hb=d7e556c576cedd722ff0115cec75e6dc09ce1da2;hp=e89169071a2cccb331b3f19b42fac8752e531b36;hpb=b56fbe62b0f248ff66b82252b01da93f9292a03f;p=libguestfs-talks.git

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 — 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>