From d29454b68e2e3fdb04282fe9c01cda6d04a47435 Mon Sep 17 00:00:00 2001
From: Yaelle Vincont <yaelle.vincont@cea.fr>
Date: Thu, 7 Nov 2019 15:49:59 +0100
Subject: [PATCH] [ref/kernel] ajout lignes et code html
---
html/kernel.html | 48 +++++++++++++++++++++++++++++-------------------
1 file changed, 29 insertions(+), 19 deletions(-)
diff --git a/html/kernel.html b/html/kernel.html
index 7c2c97b0..bff00d72 100755
--- a/html/kernel.html
+++ b/html/kernel.html
@@ -37,9 +37,9 @@ title: Kernel & Plugins - Frama-C
foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its
industrial achievements.</p>
- <p>3.1. Architecture<br>
- The Frama-C platform is written in OCaml [LDF+13], a functional language whose features are very in- teresting for
- implementing program analyzers [CSB+09]. Fig. 2 shows a functional view of the Frama-C plug-in-oriented architecture (`a
+ <h1>Architecture</h1>
+ <p>The Frama-C platform is written in OCaml [LDF+13], a functional language whose features are very in- teresting for
+ implementing program analyzers [CSB+09]. Fig. 2 shows a functional view of the Frama-C plug-in-oriented architecture (Ã
la Eclipse) whose kernel is based on a modified version of CIL [NMRW02]. CIL is a front-end for C that parses ISO C99
programs into a normalized representation. For instance, loop constructs (for, while, do & while) are given a single
normalized form, normalized expressions have no side-effects, etc. Frama-C extends CIL to support dedicated source code
@@ -49,22 +49,21 @@ title: Kernel & Plugins - Frama-C
In addition to the AST, the kernel provides several general services for helping plug-in development [SCP13] and
providing convenient features to Frama-C’s end-user.</p>
- <p>• Messages, source code and annotations are uniformly displayed.<br>
- • Parameters and command line options are homogeneously handled.<br>
- • A journal of user actions can be synthesized and replayed afterwards, a useful feature in debugging and qualification
- contexts [Sig14].<br>
- • A safe serialization mechanism [CDS11] allows the user to save results of analyses and reload them later.<br>
- • Projects, presented in Section 3.3, isolate unrelated program representations, and guarantee the integrity<br>
- of analyses.<br>
- • Consistency mechanisms control the collaboration between analyzers (Section 3.4).<br>
- • A visitor mechanism, partly inherited from CIL, facilitates crawling through the AST and writing code transformation
- plug-ins.</p>
+ <ul>
+ <li>Messages, source code and annotations are uniformly displayed.</li>
+ <li>Parameters and command line options are homogeneously handled.</li>
+ <li>A journal of user actions can be synthesized and replayed afterwards, a useful feature in debugging and qualification contexts [Sig14].</li>
+ <li>A safe serialization mechanism [CDS11] allows the user to save results of analyses and reload them later.</li>
+ <li>Projects, presented in Section 3.3, isolate unrelated program representations, and guarantee the integrity of analyses.</li>
+ <li>Consistency mechanisms control the collaboration between analyzers (Section 3.4).</li>
+ <li>A visitor mechanism, partly inherited from CIL, facilitates crawling through the AST and writing code transformation plug-ins.</li>
+ </ul>
<p>Analyzers are developed as separate plug-ins on top of the kernel. Plug-ins are dynamically linked against the kernel
to offer new analyses, or to modify existing ones. Any plug-in can register new services in a plug-in database stored in
the kernel, thereby making these services available to all plug-ins.</p>
- <p>3.2. ACSL<br>
+ <h1>ACSL</h1>
Functional properties of C programs can be expressed within Frama-C as ACSL annotations [BFH+13]. ACSL, the ANSI/ISO C
Specification Language, is a formal specification language inspired by Java’s JML [BCC+05], both being based on the
notion of function contract introduced by Eiffel [Mey97]. In its most basic form, the specification (or contract) of a
@@ -122,7 +121,10 @@ title: Kernel & Plugins - Frama-C
time the loop enters a new iteration. When both these conditions are met, we know that the loop can only be taken a
finite number of times. An example of variant for the loop in Fig. 5 would be the following: loop variant 10 - i; Each
plug-in can provide a validity status to any ACSL property and/or generate ACSL annotations. This lets ACSL annotations
- play an important role in the communication between plug-ins, as explained in Section 3.4. 3.3. Projects Frama-C allows a
+ play an important role in the communication between plug-ins, as explained in Section 3.4.</p>
+
+ <h1>Projects</h1>
+ <p>Frama-C allows a
user to work on several programs in parallel thanks to the notion of project. A project consistently stores a program
with all its required information, including results computed by analyzers and their parameters. Several projects may
coexist in memory at the same time. A non-interference theorem guarantees project partitioning [Sig09]: any modification
@@ -130,7 +132,10 @@ title: Kernel & Plugins - Frama-C
a program transformer such as E-ACSL (Section 7), Aora ̈ı (Section 8), or Slicing (Section 10.1) is used. The result of
the transformation is a fresh AST that coexists with the original one, making backtracking and comparisons easy. This is
illustrated in Section 10.2. Another use of projects is to process the same program in different ways – for instance
- with different analysis parameters. 3.4. Collaborations across analyzers In Frama-C, analyzers can interoperate in two
+ with different analysis parameters.</p>
+
+ <h1>Collaborations across analyzers</h1>
+ In Frama-C, analyzers can interoperate in two
different ways: either sequentially, by chaining analysis results to perform complex operations; or in parallel, by
combining partial analysis results into a full program verification. The former consists in using the results of an
analyzer as input to another one thanks to the plug-in database stored by the Frama-C kernel. Refer to Section 10.1 for
@@ -145,14 +150,19 @@ title: Kernel & Plugins - Frama-C
runtime by leveraging the E-ACSL plug-in (Section 7). The kernel automatically computes the validity status of each
program property from the information provided by all analyzers and ensures the correctness of the entire verification
process. For that, plug-ins can set the local validity status of an ACSL property, together with its set of dependencies.
- Those dependencies can be: • other ACSL properties that are assumed to be true; • the reachability of a statement;
- • some parameters of the plug-in that set a hypothesis over the memory state of the program. With this information, the
+ Those dependencies can be:</p>
+ <ul>
+ <li>other ACSL properties that are assumed to be true;</li>
+ <li>the reachability of a statement;</li>
+ <li>some parameters of the plug-in that set a hypothesis over the memory state of the program.</li>
+ </ul>
+ <p>With this information, the
kernel can then compute a consolidated validity status for each ACSL property. [CS12] presents the algorithm that is used
for that purpose. Its main correctness property can be stated as: “if the consolidated status of a property is computed
as valid [resp. invalid] by the kernel, then the property is valid [resp. invalid] with respect to ACSL semanticsâ€.
This algorithm is also complete:“if a property is proven valid [resp. invalid] by at least one analyzer, then its
computed consolidated status is valid [resp. invalid] as soon as one other analyzer does not prove the contrary, in which
- case the special status ‘inconsistent’ is computed.â€1</p>
+ case the special status ‘inconsistent’ is computed.â€</p>
<div class="aboutKernel">
<h2 class="subTitle">Some articles about kernal sections</h2>
--
GitLab