diff --git a/_fc-plugins/dive.md b/_fc-plugins/dive.md new file mode 100644 index 0000000000000000000000000000000000000000..01d7d7c34564b8f9793043bd2c49774a45f09c7c --- /dev/null +++ b/_fc-plugins/dive.md @@ -0,0 +1,73 @@ +--- +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. + + + +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. diff --git a/assets/img/plugins/dive.png b/assets/img/plugins/dive.png new file mode 100644 index 0000000000000000000000000000000000000000..27ab20ef35b8212b320dd098f936c9078c9d71b3 Binary files /dev/null and b/assets/img/plugins/dive.png differ