diff --git a/_layouts/post.html b/_layouts/post.html
index 36af906a5596105d93313cede6e70af4a440a3c9..972719f9443a31ce666b0fc33df6a111aad7c552 100644
--- a/_layouts/post.html
+++ b/_layouts/post.html
@@ -1,64 +1,64 @@
----
-layout: default
----
-
- <div id="wrapper" class="hfeed">
-
- {% include headers.html header=5 title=Blog %}
-
- <div id="container" class="mainContainer">
- <div class="defaultPage blogsPage singleBlogPage" id="content" role="main">
- <div class="contentWrap">
- <div class="breadcrumb backNavigation">
- <a href="/blog/index.html" class="backLink2"><i class="icon icon-arrow-left"></i> Back to blogs</a>
- </div>
- </div>
-
- <div class="contentWrap">
- <div class="blogsSection">
- <div class="blogsSectionContent singleBlog">
- <div class="imageBlogPage" style=
- "background-image: url({% if page.image %}{{ page.image }}{% else %}/assets/img/default-blog.jpg{% endif %});">
- </div>
- <article>
- <div class="blogNav">
- {% if page.previous.url %}
- <span class="blogNavPost left"><a class="prevPost" href="{{page.previous.url}}">← {{ page.previous.title }}</a></span>
- {% endif %}
- {% if page.next.url %}
- <span class="blogNavPost right"><a class="nextPost" href="{{page.next.url}}">{{page.next.title }} →</a></span>
- {% endif %}
- </div>
-
- <h1 id="blogPostTitle"><span>{{ page.title }}</span></h1>
-
- <address class="blogPostAddress">
- {{ page.author }} - {{ page.date | date_to_string: "ordinal" }}
- </address>
- <div class="content">
- {{ content }}
- </div>
- </article>
-
- <address class="blogPostAddress" style="text-align: right;">
- {{ page.author }}
- <br>{{ page.date | date_to_string: "ordinal" }}
- </address>
- <br>
- <div class="blogNav">
- {% if page.previous.url %}
- <span class="blogNavPost left"><a class="prevPost" href="{{page.previous.url}}">← {{ page.previous.title }}</a></span>
- {% endif %}
- {% if page.next.url %}
- <span class="blogNavPost right"><a class="nextPost" href="{{page.next.url}}">{{ page.next.title }} →</a></span>
- {% endif %}
- </div>
- </div>
-
- {% include sidebar_blog.html cats=page.categories %}
- </div>
- </div>
- </div>
- {% include footer.html %}
- </div>
- </div>
+---
+layout: default
+---
+
+ <div id="wrapper" class="hfeed">
+
+ {% include headers.html header=4 title=Blog %}
+
+ <div id="container" class="mainContainer">
+ <div class="defaultPage blogsPage singleBlogPage" id="content" role="main">
+ <div class="contentWrap">
+ <div class="breadcrumb backNavigation">
+ <a href="/blog/index.html" class="backLink2"><i class="icon icon-arrow-left"></i> Back to blogs</a>
+ </div>
+ </div>
+
+ <div class="contentWrap">
+ <div class="blogsSection">
+ <div class="blogsSectionContent singleBlog">
+ <div class="imageBlogPage" style=
+ "background-image: url({% if page.image %}{{ page.image }}{% else %}/assets/img/default-blog.jpg{% endif %});">
+ </div>
+ <article>
+ <div class="blogNav">
+ {% if page.previous.url %}
+ <span class="blogNavPost left"><a class="prevPost" href="{{page.previous.url}}">← {{ page.previous.title }}</a></span>
+ {% endif %}
+ {% if page.next.url %}
+ <span class="blogNavPost right"><a class="nextPost" href="{{page.next.url}}">{{page.next.title }} →</a></span>
+ {% endif %}
+ </div>
+
+ <h1 id="blogPostTitle"><span>{{ page.title }}</span></h1>
+
+ <address class="blogPostAddress">
+ {{ page.author }} - {{ page.date | date_to_string: "ordinal" }}
+ </address>
+ <div class="content">
+ {{ content }}
+ </div>
+ </article>
+
+ <address class="blogPostAddress" style="text-align: right;">
+ {{ page.author }}
+ <br>{{ page.date | date_to_string: "ordinal" }}
+ </address>
+ <br>
+ <div class="blogNav">
+ {% if page.previous.url %}
+ <span class="blogNavPost left"><a class="prevPost" href="{{page.previous.url}}">← {{ page.previous.title }}</a></span>
+ {% endif %}
+ {% if page.next.url %}
+ <span class="blogNavPost right"><a class="nextPost" href="{{page.next.url}}">{{ page.next.title }} →</a></span>
+ {% endif %}
+ </div>
+ </div>
+
+ {% include sidebar_blog.html cats=page.categories %}
+ </div>
+ </div>
+ </div>
+ {% include footer.html %}
+ </div>
+ </div>
diff --git a/assets/css/page.css b/assets/css/page.css
index a4dcb3acc96123b18f0b0a55f5f059bb9e403b27..e0debe16f6c8dbfb7261c1f320ef78f194d6e9d1 100644
--- a/assets/css/page.css
+++ b/assets/css/page.css
@@ -1230,3 +1230,54 @@ details summary:before {
transform: translateY(-10px);
}
}
+
+.sidecode {
+ width: 50%;
+ overflow: hidden;
+ margin-bottom: 20px;
+}
+@media (min-width: 1024px) {
+ .sidecode {
+ margin-bottom: 25px;
+ }
+}
+.sidecode pre {
+ width: 90%;
+ margin-left: auto;
+ margin-right: auto;
+}
+sidenote {
+ position: absolute;
+ width: 45%;
+ margin-right: 5%;
+ right: -12px;
+ padding-left: 11px;
+ border-left: 3px solid #e9b040;
+ font-family: 'Muli';
+ font-size: 14px;
+ text-align: justify;
+ white-space: pre-wrap;
+}
+@media (min-width: 768px) {
+ sidenote {
+ font-size: 15px;
+ }
+}
+@media (min-width: 1024px) {
+ sidenote {
+ font-size: 16px;
+ }
+}
+@media (min-width: 1600px) {
+ sidenote {
+ font-size: 17px;
+ }
+}
+sidenote + point {
+ content:'';
+ display: inline-block;
+ width: 100%;
+ margin: 0 -100% 0 .5em;
+ vertical-align: middle;
+ border-bottom: 1px solid #e9b040;
+}
diff --git a/html/acsl.html b/html/acsl.html
index 5ffe2036ad9e751038cedf241bf8539f41c2996c..a8b5ad803c59a092b06eafe338578cfa3be32343 100755
--- a/html/acsl.html
+++ b/html/acsl.html
@@ -6,6 +6,7 @@ active: 4
---
<h1>ANSI/ISO C Specification Language</h1>
+
<h2>Quick description</h2>
<p>The ANSI/ISO C Specification Langage (ACSL) is a behavioral
specification language for C programs. The design of ACSL is
@@ -23,37 +24,47 @@ software, they generally leave the actual expression of the
contract to run-time assertions, or to comments in the source code.
ACSL is expressly designed for writing the kind of properties that
make up a function contract.
-ACSL is a <em>formal</em> language. This means that the
-specifications written in ACSL can be automatically manipulated by
-helper programs, in the same way that a programming language is a
-formal language manipulated by a compiler, and by opposition to
-informally written comments that can only be useful to humans.</p>
+ACSL is a <em>formal</em> language.</p>
+
+<div class="sidecode">
+<pre>
+/*@
+ requires \valid(a+(0..n-1));<sidenote>ACSL provides specification primitives to cover the low-level aspects of the C programming language</sidenote><point></point>
+
+ assigns a[0..n-1];
+
+ ensures<sidenote>As a formal language, ACSL enables a precise specification of function contracts. That makes the specification not only understandable by a human, but also manipulable by an analyzer. Furthermore, as a complete specification is not always useful, the contract can be partial, it depends on what one wants to verify.</sidenote><point></point>
+ \forall integer i;
+ 0 <= i < n ==> a[i] == 0;
+*/
+void set_to_0(int* a, int n){
+ int i;
-<p>ACSL allows to write contracts that range from the low-level
-(“<i>this function expects a valid pointer to int</i>â€) to the
-high-level (“<i>this function expects a nonempty linked list of
- ints and returns the greatest of these ints</i>â€). It is expressive
-enough to write complete specifications for many functions, but it
-can also be used for writing partial specifications. Partial
-specifications, of which the “<i>expects a valid pointer to
- int</i>†contract is a typical example, do not describe completely
-the expected behavior of the function. Function contracts written as
-run-time assertions are almost always partial specifications,
-because a complete specification would be too annoying to write in
-the same language as the programming language (indeed, most often
-this would mean programming the function a second time).</p>
+ /*@
+ loop invariant 0 <= i <= n;
+ loop invariant
+ \forall integer j;<sidenote>It also allows more abstract reasoning through mathematical or logic types, or through the definition of high level ideas, like "the function expects a valid linked list".</sidenote><point></point>
+ 0 <= j < i ==> a[j] == 0;
+ loop assigns i, a[0..n-1];
+ loop variant n-i;
+ */
+ for(i = 0; i < n; ++i)
+ a[i] = 0;
+}
+</pre>
+</div>
<p><a href="../fc-plugins/wp.html">WP</a> and the older
<a href="../fc-plugins/jessie.html">Jessie</a>
plug-ins use Hoare-style weakest precondition computations to
formally prove ACSL properties. The process can be quite automatic,
-thanks to external theorem provers such as Alt-Ergo, Z3 or CVC4
+thanks to external theorem provers such as Alt-Ergo, Z3 or CVC4,
or more interactive, with WP's built-in interactive prover
-or the use of the Coq proof-assistant. Other
+or the use of the Coq proof assistant. Other
plug-ins, such as the <a href="../fc-plugins/eva.html">Eva</a>
plug-in, may
also contribute to the verification of ACSL properties. They may
-also report static analysis results in terms of asserted new ACSL
+also report static analysis results in terms of new asserted ACSL
properties inside the source code.</p>
<h2>More information</h2>
diff --git a/html/kernel.html b/html/kernel.html
index 7f7a60024dbb8ec3af8061bcb632c6cd73d14ed8..757b0770caa3079a486d1db91467d176a5598b0a 100755
--- a/html/kernel.html
+++ b/html/kernel.html
@@ -4,142 +4,76 @@ css: plugin
title: Kernel & Plugins - Frama-C
active: 2
---
-<p>WIP (TA)</p>
-<p>The Frama-C kernel acts as a <em>lingua franca</em> for all <a href=
-"https://frama-c.frama-c.com/html/kernel-plugin.html">Frama-C plugins</a>. A software analysis platform that
-checks security, verifies requirements, and guarantees trust in C programs.</p>
-
-<p>Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It
-provides its users with a collection of plug-ins that perform static analysis, deductive verification, and testing, for
-safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their
-integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This
-foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its
-industrial achievements.</p>
+<p>The Frama-C platform allows checking security, verifying requirements and
+ guaranteeing trust in C programs, thanks to a collection of collaborative
+ <a href="/html/kernel-plugin.html">plugins</a> that
+ perform static and dynamic analysis, for safety- and
+ security-critical software. Collaborative verification across cooperating
+ plug-ins is enabled by their integration on top of a shared kernel and
+ datastructures, and their compliance to
+ <a href="/html/acsl.html">a common specification language</a>.
+</p>
<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
-annotations expressed in ACSL (see Section 3.2). This modified CIL front-end produces the C + ACSL abstract syntax tree
-(AST), an abstract view of the program shared among all analyzers. This AST takes into account machine-dependent
-parameters (size of integral types, endianness, etc.) which can easily be modified by the end-user.<br>
-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>The Frama-C kernel is based on a modified version of
+ <a href="https://link.springer.com/chapter/10.1007/3-540-45937-5_16">CIL</a>.
+ CIL is a front-end for C that parses ISO C99 programs into a normalized
+ representation. Frama-C extends CIL to support
+ <a href="/html/acsl.html">ACSL</a>.
+ This modified CIL front-end produces the C + ACSL abstract syntax tree (AST),
+ an abstract view of the program shared among all analyzers. In addition to the
+ AST, the kernel provides several general services.
+</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>
+<li>Messages, source code and annotations are uniformly displayed</li>
+<li>Parameters and command line options are homogeneously handled</li>
+<li>A serialization mechanism allows the user to save results of analyses
+ and reload them later</li>
+<li>Projects isolate unrelated program representations, and guarantee the
+ integrity of analyses</li>
+<li>Consistency mechanisms control the collaboration between analyzers</li>
+<li>A visitor mechanism 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>
-
-<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
-function states the pre-conditions it requires from its caller and the post- conditions it ensures when returning. Among
-these post-conditions, one kind of clause plays a particular role by saying which memory locations the function assigns,
-i.e. which locations might have a different value between the pre- and the post-state. Conversely, any memory location
-not mentioned in this clause is supposed to be left unmodified by the function.<br>
-Annotations are written in first-order logic, and it is possible to define custom functions and predicates for use in
-annotations together with ACSL built-ins. Indeed, ACSL features its own functions and predicates to describe memory
-states. However, it does not introduce any notion beyond the C standard, leaving each plug-in free to perform its own
-abstractions over the concrete memory layout.</p>
-
-<p>For instance, Fig. 3 provides a formal ACSL specification for a swap function. Informally, swap is supposed to
-exchange the content of two (valid) pointer cells given as argument.<br>
-The first pre-condition states that the two arguments must be valid int pointers, i.e. that dereferencing a or b will not
-produce a run-time error. In addition, the second pre-condition asks that the two locations do not overlap. \valid and
-\separated are two built-in ACSL predicates.<br>
-The assigns clause states that only the locations pointed to by a and b might be modified by a call to swap; any other
-memory location is untouched. Finally, the post-condition says that at the end of the function, *a contains the value
-that was in *b in the pre-state, and vice versa.<br>
-Function contracts can also be structured into behaviors. In addition to the clauses described above, a behavior can be
-guarded by assumes clauses, which specify under which conditions the behavior is activated. This provides a convenient
-way to distinguish various cases under which the function can be called. Behaviors do not need to be either complete (at
-least one behavior is active for any given call) or disjoint (there is at most one behavior active for a given call), but
-this can be stipulated with the appropriate clauses in order to check that the specification is correct in this respect.
-As an example, Fig. 4 presents the specification of a function swap_or_null similar to swap except that it will attempt
-to swap contents only when both pointers are non-null. This corresponds to the behavior not_null, in which case the
-function expects to have valid (in C a non-null pointer is not necessarily valid) and separated pointers and will act as
-above. On the other hand, in the null case, the function does nothing: at least one pointer is null, so the values cannot
-be swapped. We are always in exactly one of these two cases, so null and not_null are clearly complete and disjoint.<br>
-In addition to function specifications, ACSL offers the possibility of writing annotations in the code, in the form of
-assertions, properties that must be true at a given point, or loop invariants, properties that are true for each loop
-step. More precisely, a loop invariant is associated to a for, while, or do & while loop. It must hold when arriving at
-the loop entry for the first time, and must be preserved by a loop step. That is, if we enter the loop body in a state
-that verifies the invariant, then the invariant must hold at the end of the block – except if we exit from the block
-through goto, break or continue. With these two properties, we can then prove by induction that the invariant is true for
-any number of loop steps<br>
-(including 0). As with assigns clauses in function contracts, loop assigns clauses are a particular case of invariant
-that state which memory locations might have been modified since the beginning of the loop (implicitly stating that all
-other locations are not modified by the loop). Loop invariants are required for<br>
-deductive verification (see Section 5).</p>
-
-<p>As an example, Fig. 5 presents a simple for loop initializing the elements of an array, together with its associated
-invariants. The first invariant specifies the bounds of the index of the loop. Note that the invariant uses i<=10,
-while the test in the code is i<10. Indeed, the invariant must be preserved by any step of the loop, including the
-last one, in which i is equal to 10 at the end of the step. The second invariant states that the i-1 first cells of the
-array have been initialized. It is true before entering the loop, as there is no j such that 0<=j<0, so the
-implication is trivially true. Then, if we suppose that the invariant holds at the beginning of a loop step, the step
-will initialize cell i and increment i, so that the invariant is still true af the end of the step. Similarly, the loop
-assigns clause indicates that the loop has potentially modified i and the first i-1 cells of the array. Namely, this is
-true when entering the loop (nothing has been modified), and if we suppose that only i and the beginning of the array has
-been assigned, the next loop step also assigns i and the ith cell, again making the invariant true at the end of the
-step. Loop invariants are not concerned with termination. Instead, termination can be ensured through the special clause
-loop variant. It requires an integer expression that strictly decreases during a loop step, while remaining positive each
-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.</p>
+<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>
<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
-on a value of a project P does not impact a value of another project P′. Such a feature is of particular interest when
-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.</p>
+<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. The
+ projects are partitioned so that a modification on a particular projet does
+ not impact the others. The project mechanism may also be used for example
+ to perform different code transformations on the same original project, or to
+ execute a particular analysis on the same project but with different
+ 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
-an illustration of a sequential analysis. The parallel collaboration of analyzers consists in verifying a program by
-heterogeneous means. ACSL is used to this end as a collaborative language: plug-ins generate program annotations, which
-are then vali- dated by other plug-ins. Partial results coming from various plug-ins are integrated by the kernel to
-provide a consolidated status of the validity of all ACSL properties. For instance, when the Value plug-in (Section 4) is
-unable to ensure the validity of a pointer p, it emits an unproved ACSL annotation assert \valid(p). ACSL’s blocking
-semantics states that an execution trace leading to an invalid property stops its execu- tion (see [GGJK08, HMM12,
-CS12]). Thus, Value can assume that p is valid from this program point onwards, since the execution can only continue if
-the assert is valid. The WP plug-in (Section 5) may later be used to prove this hypothesis, or it can be checked at
-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:</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.â€</p>
\ No newline at end of file
+
+<p>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.
+ The parallel collaboration of analyzers consists in verifying a program by
+ heterogeneous means. ACSL is used to this end as a collaborative language:
+ plug-ins generate program annotations, which are then validated by other
+ plug-ins. Partial results coming from various plug-ins are integrated by the
+ kernel to provide a consolidated status of the validity of all ACSL
+ properties. 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.
+</p>
+<p>The main correctness property of the Frama-C kernel 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".
+</p>