[plugins] add Dive plug-in description page

_fc-plugins/dive.md

+---
+layout: plugin
+title: Dive
+description: Dive provides dataflow visualization (from Eva) in Ivette.
+key: browsing
+distrib_mode: main
+---
+
+## Overview
+
+The **Dive** plug-in provides dataflow visualization in [Ivette](ivette.html).
+It displays graphs with information provided by [Eva](eva.html) and
+[Studia](studia.html), such as value ranges of expressions,
+dependency information (e.g. which memory areas impact a given expression),
+taint information, between others.
+
+This information is displayed in a dynamic graph (using various layout
+algorithms) which can be interacted with, allowing for faster understanding
+of the causes of an alarm, or loss of precision during the analysis.
+
+## Quick Start
+
+Copy the example code below into a file named `dive.c`, then run:
+
+    ivette -eva dive.c
+
+Open the *Dive Dataflow* view in the upper right corner.
+
+An alarm (represented with an ACSL annotation) will be present before the
+`arr[1] = 1;` statement in the *AST* panel. Click on it, and you should
+obtain a graph similar to the one below.
+
+![Dive plug-in screenshot](/assets/img/plugins/dive.png)
+
+You can click to expand nodes, and hover to obtain the value range as well as
+the value type. The node color indicates the precision of the value range.
+Arrows point from each dependency to its dependent location.
+
+### Example code
+
+```
+// dive.c
+#include <__fc_builtin.h>
+volatile int nondet;
+unsigned f(char a, unsigned b, unsigned c) {
+  unsigned res;
+  if (b > 10) {
+    res = 5;
+  } else if (b > 1) {
+    res = a;
+  } else {
+    res = c / 2;
+  }
+  return res;
+}
+
+int main(void) {
+  char a = 42;
+  unsigned b = Frama_C_unsigned_int_interval(0, 100);
+  unsigned c = Frama_C_unsigned_int_interval(0, (unsigned)-1);
+  unsigned r = f(a, b, c);
+  char arr[100];
+  arr[r] = 1; // alarm
+  return 0;
+}
+```
+
+## Technical Notes
+
+- Maturity: experimental
+
+- Automatically available in Ivette; results displayed in *Dive Dataflow*
+  view when Eva has been executed.