[GUI] add feature page for GUI

_data/tabs.yml

@@ -2,7 +2,7 @@
   link: /html/kernel-plugin.html
 - name: Kernel
   link: /html/kernel.html
-- name: ACSL
-  link: /html/acsl.html
 - name: GUI
   link: /html/gui.html
+- name: ACSL
+  link: /html/acsl.html

html/acsl.html

@@ -2,7 +2,7 @@
 layout: feature
 css: plugin
 title: ACSL
-active: 3
+active: 4
 ---
 
 <h1>ANSI/ISO C Specification Language</h1>

html/gui.md

+---
+layout: feature
+css: plugin
+title: Graphical User Interface (GUI) - Frama-C
+active: 3
+---
+
+If the Frama-C kernel is the heart of the platform,
+the Graphical User Interface (GUI) is its head:
+it enables exploring the code, augmented with several navigation tools and
+highlighting modes; it allows launching, parametrizing and visualizing analyses;
+and it allows combining them seamlessly, taking full advantage of the
+multi-paradigm approach.
+
+## Architecture
+
+The Frama-C GUI is implemented in OCaml, using a GTK-based graphical framework
+([lablgtk](http://lablgtk.forge.ocamlcore.org/)) written in OCaml.
+
+It is implemented as a *plug-in*, albeit a special one; it is enabled by
+running a different binary than the command line Frama-C.
+
+## AST Code Browsing
+
+The most basic usage of the Frama-C GUI consists in providing a navigable view
+of the source code. The Frama-C kernel, after preprocessing and normalizing
+the code, produces an internal representation (called an *Abstract Syntax Tree*,
+AST for short) which is slightly different from the original source code.
+The Frama-C GUI displays both versions side-to-side, as in the screenshot below.
+
+![Normalized and original source code in the GUI](/assets/img/gui/gui-hello-world.png)
+
+The internal code representation seen by Frama-C, often called
+*normalized code*, or *CIL code* (see [Kernel](kernel.html) for details),
+is presented in the left panel, which is typically in the center of the
+graphical interface. The original code is presented in the right.
+
+This simple, *hello world!*-style code allows us to see some operations
+performed by Frama-C:
+
+- Code normalization: loop normalization, a single return point per function,
+  pointer dereferencing (e.g. `i[s]` becomes `*(s+i)`);
+- Implicit conversions are made explicit (e.g. the string literal of type
+  `const char *` is cast to `char *`).
+- Code understanding: selecting an expression in the GUI (highlighted in green
+  in the above screenshot) displays its syntatic properties (*Information* tab)
+  and the corresponding line in the source code.
+
+## Plug-in Integration
+
+Many Frama-C plug-ins are integrated into the GUI: they add panels,
+controls and displays, to bring useful information to the user in the
+most efficient way possible.
+
+![GUI with Integrated Plugins](/assets/img/gui/gui-plugin-integration.png)
+
+In the screenshot above, we see, on the left, the *file tree* panel, which
+displays the list of globals (functions and variables) in the program.
+In this case, the [Metrics](metrics.html) and [Eva](eva.html) plug-ins were
+enabled, and the file tree display includes three extra columns: percentage
+of dead code, number of dead statements, and total number of statements per
+function.
+
+The user can sort by any of these columns, and a right-click enables a series
+of filters on them. `Ctrl+F` enables textual search. Unreachable function names
+are crossed out.
+
+All of this information can be obtained via reports and in textual form, but
+their tight integration in the GUI greatly increases productivity and the
+semantic understanding of a code base. The screenshot below showcases several
+plug-ins having graphical components integrated into the GUI.
+
+![Plugin Panels in the GUI](/assets/img/gui/gui-plugin-panels.png)
+
+## Parametrization of Analyses
+
+The Frama-C GUI allows parametrizing and re-running analyses.
+
+![GUI Analyses Manager](/assets/img/gui/gui-analyses.png)
+
+## Deep Semantic Analysis
+
+Besides the syntactic facilities, the Frama-C GUI is especially useful to
+handle the semantic properties which are the specialty of the Frama-C
+framework.
+
+All properties of interest (runtime errors, function contracts, etc.) are
+displayed in the GUI as [ACSL](acsl.html) annotations interspersed with
+the code, with colored markers indicating their current status in the
+platform (*valid*, *invalid*, *unknown*, *no proof attempted*, etc.).
+A filterable list allows inspecting them and quickly navigating the code
+to find the points of interest.
+
+![GUI Properties and Statuses](/assets/img/gui/gui-properties.png)
+
+In the example above, the original code contained a call to a `COPY` macro,
+which in fact calls the library function `memcpy`. That function, along with
+several others in the standard C library, has an [ACSL](acsl.html)
+specification provided by the Frama-C team. That specification establishes
+some properties which must be verified to ensure the absence of runtime errors
+(e.g., the destination must point to valid memory). These properties are
+displayed by the GUI at the point where they must be verified. They have a
+green circle next to them, indicating that at least one Frama-C plug-in was
+able to prove them.
+
+Conversely, the yellow circle before the `if`, at the beginning of the function,
+indicates that a plug-in (Eva, in this case) attempted to prove the property
+but was unable to; another plug-in may try it and update the status accordingly.
+
+## Technical Notes
+
+- The GUI is not an editor; it allows code inspection and navigation, including
+  to the original source (e.g. Ctrl+clicking the original source), but not
+  live-editing.
+- Initial source preparation and parsing (before obtaining a valid AST) is more
+  suitable for the command-line Frama-C interface. Frama-C's *session* mechanism
+  allows loading the result to combine it with other analyses and displaying
+  the result in the GUI.