diff --git a/_data/tabs.yml b/_data/tabs.yml index 0286c5ab332309e8576e5815c260c96fa7f8a1a3..d5032da222a141fe5c4f5f935f569d262e6ebf08 100644 --- a/_data/tabs.yml +++ b/_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 diff --git a/assets/img/gui/gui-analyses.png b/assets/img/gui/gui-analyses.png new file mode 100644 index 0000000000000000000000000000000000000000..2f3cdde9de5ef6bf85cb9891e336109d04da636b Binary files /dev/null and b/assets/img/gui/gui-analyses.png differ diff --git a/assets/img/gui/gui-hello-world.png b/assets/img/gui/gui-hello-world.png new file mode 100644 index 0000000000000000000000000000000000000000..f6f6a56fa0857f5be33cfabf1161e3c4eb9fadcd Binary files /dev/null and b/assets/img/gui/gui-hello-world.png differ diff --git a/assets/img/gui/gui-plugin-integration.png b/assets/img/gui/gui-plugin-integration.png new file mode 100644 index 0000000000000000000000000000000000000000..d235ff60f589382ecbfea468d86e49cc79e2f8c2 Binary files /dev/null and b/assets/img/gui/gui-plugin-integration.png differ diff --git a/assets/img/gui/gui-plugin-panels.png b/assets/img/gui/gui-plugin-panels.png new file mode 100644 index 0000000000000000000000000000000000000000..5796ecfa0ed1e617421381f3dec4145959c9b77a Binary files /dev/null and b/assets/img/gui/gui-plugin-panels.png differ diff --git a/assets/img/gui/gui-properties.png b/assets/img/gui/gui-properties.png new file mode 100644 index 0000000000000000000000000000000000000000..69a70db7b6feecae35ea07d4252c3e520442f68d Binary files /dev/null and b/assets/img/gui/gui-properties.png differ diff --git a/html/acsl.html b/html/acsl.html index 66e4edc9be4ef621f81b96dce6fb043ee35c747b..5ffe2036ad9e751038cedf241bf8539f41c2996c 100755 --- a/html/acsl.html +++ b/html/acsl.html @@ -2,7 +2,7 @@ layout: feature css: plugin title: ACSL -active: 3 +active: 4 --- <h1>ANSI/ISO C Specification Language</h1> diff --git a/html/gui.md b/html/gui.md new file mode 100644 index 0000000000000000000000000000000000000000..103841e8001cc5ece51059a9d1dc20ab53a26185 --- /dev/null +++ b/html/gui.md @@ -0,0 +1,118 @@ +--- +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. + + + +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. + + + +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. + + + +## Parametrization of Analyses + +The Frama-C GUI allows parametrizing and re-running analyses. + + + +## 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. + + + +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.