diff --git a/assets/img/author/inria.jpg b/assets/img/author/inria.jpg
deleted file mode 100644
index e000305f0f7e3d00a4312df654a2813b5d2a5885..0000000000000000000000000000000000000000
Binary files a/assets/img/author/inria.jpg and /dev/null differ
diff --git a/assets/img/author/inria.png b/assets/img/author/inria.png
new file mode 100644
index 0000000000000000000000000000000000000000..4663638d7189764401570b2054cd1d30dfa08f74
Binary files /dev/null and b/assets/img/author/inria.png differ
diff --git a/html/authors.html b/html/authors.html
index 3dca5f61e27d46231a385716a5598b708e357b25..5be85603af12a9a1b0d7ff39c9ba2300fd4e0b93 100755
--- a/html/authors.html
+++ b/html/authors.html
@@ -4,7 +4,7 @@ title: Authors - Frama-C
---
<body class="page-template page-template-page-authors page-template-page-authors-php page page-id-231 nonTouch">
<div id="wrapper" class="hfeed">
-
+
{% include headers.html %}
<div id="container" class="mainContainer">
@@ -36,10 +36,10 @@ title: Authors - Frama-C
<div class="authorInfo">
<figure>
- <img src="/assets/img/author/inria.jpg">
+ <img src="/assets/img/author/inria.png">
</figure>
- <p><span class="title">INRIA Saclay - ILe - De - France</span> Toccata team, common with LRI-CNRS and
+ <p><span class="title">Inria Saclay - ÃŽle-de-France</span> Toccata team, common with LRI-CNRS and
Université Paris-Sud 11</p>
</div>
</div>
@@ -66,7 +66,7 @@ title: Authors - Frama-C
<section id="comments" style="display: none;"></section>
</div>
-
+
{% include footer.html %}
<div class="clear"></div>
diff --git a/html/careers.html b/html/careers.html
index 0b346dc860d7553a8d7a9a0d5dcb4590c09f8992..6a8abdd765c13d8ea495ec3acd45d6f354b8f5cc 100755
--- a/html/careers.html
+++ b/html/careers.html
@@ -6,9 +6,9 @@ title: Careers at Frama-C
<body class="page-template page-template-page-careers page-template-page-careers-php page page-id-146 nonTouch">
<div id="wrapper" class="hfeed">
-
+
{% include headers.html header=6 %}
-
+
<div id="container" class="mainContainer">
<div class="pageCareers pages">
<div class="bgTextbig">
@@ -20,13 +20,13 @@ title: Careers at Frama-C
<div class="pageBanner" style=
"background-image:url('https://framac.s3.amazonaws.com/staging/uploads/2017/07/banner.jpg');background-size: cover;">
- <p>Which job is done for you?</p>
+ <p>Which job is made for you?</p>
</div>
<h3 class="subTitle">Go Corporate at FRAMA-C</h3>
<div class="careerList">
-
+
{% for job in site.jobs %}
<a class="listItem" href="{{ job.url }}">
<h4 class="listItemTitle" data-bgtext="{{ job.title }}">{{ job.title }}</h4>
diff --git a/html/contact.html b/html/contact.html
index 0be931f12718bb13f39ea7d4c02db205707a5c2d..04eacd3b5067de3d893a1037575e867fc3a4f851 100755
--- a/html/contact.html
+++ b/html/contact.html
@@ -87,12 +87,12 @@ function(err, data) {
<div class="leftBlock">
<div class="inputWrap">
- <div class="textError"></div><input type="text" name="name" placeholder="Name" class="textbox" data-parsley-required=
+ <div class="textError"></div><input type="text" name="name" placeholder="Your name" class="textbox" data-parsley-required=
"" data-parsley-pattern="^[a-zA-Z_ ]+$" data-parsley-errors-container=".textError">
</div>
<div class="inputWrap">
- <div class="emailError"></div><input type="email" name="email" placeholder="Email" class="textbox"
+ <div class="emailError"></div><input type="email" name="email" placeholder="Your email" class="textbox"
data-parsley-required="" data-parsley-errors-container=".emailError">
</div>
@@ -100,18 +100,18 @@ function(err, data) {
<div class="radioError"></div><span>You are:</span>
<p><input id="radio1" name="you_are" type="radio" value="An Academic" data-parsley-required=""
- data-parsley-errors-container=".radioError"> <label for="radio1">An Academic</label></p>
+ data-parsley-errors-container=".radioError"> <label for="radio1">An academic</label></p>
<p><input id="radio2" name="you_are" type="radio" value="An Industrial" data-parsley-required=""
data-parsley-errors-container=".radioError"> <label for="radio2">An industrial</label></p>
<p><input id="radio3" name="you_are" type="radio" value="An Applicant" data-parsley-required=""
- data-parsley-errors-container=".radioError"> <label for="radio3">An Applicant</label></p>
+ data-parsley-errors-container=".radioError"> <label for="radio3">A candidate</label></p>
</div>
</div>
<div class="messageWrap">
- <span>Type your message</span>
+ <span>Type your message</span>
<textarea id="contact_textarea" name="message" placeholder="Your message" data-parsley-required=""
data-parsley-errors-container=".textareaError" maxlength="220">
</textarea>
@@ -138,89 +138,96 @@ function(err, data) {
<p>If you think Frama-C could be part of any kind of scientific collaboration, including research projects, internships,
PhDs, post-doctoral positions and dissemination activities,</p>
- <p><a href="mailto:florent.kirchner@cea.fr">Florent.Kirchner@cea.fr</a><small>|</small><a href=
- "mailto:loic.correnson@cea.fr">Loic.Correnson@cea.fr</a></p>
+ <p><a href="mailto:florent.kirchner@cea.fr">florent.kirchner(at)cea.fr</a><small>|</small><a href=
+ "mailto:loic.correnson@cea.fr">loic.correnson(at)cea.fr</a></p>
</div>
-
+
<div class="usefulLinks" id="side-content">
<h3 class="subTitle">Community</h3>
<div id="sidebar-content">
- <ul class="side-feed">
- <li class="icon_1">
- <a href="https://bts.frama-c.com/my_view_page.php" target="_blank">
- <div class="slideCaption">
- Bug Tracker
- </div>
-
- <div class="description">
- The official Frama-C bug tracking system (BTS).
- </div></a>
- </li>
-
- <li class="icon_2">
- <a href="https://stackoverflow.com/tags/frama-c/" target="_blank">
- <div class="slideCaption">
- Stack Overflow
- </div>
-
- <div class="description">
- The Frama-C community uses Stack Overflow for general-purpose questions.
- </div></a>
- </li>
-
- <li class="icon_3">
- <a href="https://lists.gforge.inria.fr/pipermail/frama-c-discuss/" target="_blank">
- <div class="slideCaption">
- Frama-C-discuss
- </div>
-
- <div class="description">
- The official Frama-C mailing list (announcements and general questions).
- </div></a>
- </li>
-
- <li class="icon_4">
- <a href="https://github.com/frama-c" target="_blank">
- <div class="slideCaption">
- Frama-C on Github
- </div>
-
- <div class="description">
- Frama-C snapshots and related code bases (Qed, open source case studies...).
- </div></a>
- </li>
-
- <li class="icon_5">
- <a href="https://github.com/acsl-language" target="_blank">
- <div class="slideCaption">
- ACSL on Github
- </div>
-
- <div class="description">
- Official Github repositories for the ANSI/ISO C Specification Language (ACSL).
- </div></a>
- </li>
-
- <li class="icon_6">
- <a href="/html/careers.html" target="_blank">
- <div class="slideCaption">
- Careers
- </div>
-
- <div class="description">
- Reference site about Lorem Ipsum, giving information on its origins, as well as a random Lipsum generator.
- </div></a>
- </li>
- </ul>
+ <ul class="side-feed">
+ <li class="icon_1">
+ <a href="https://bts.frama-c.com/my_view_page.php" target="_blank">
+ <div class="slideCaption">
+ Bug Tracker
+ </div>
+
+ <div class="description">
+ The official Frama-C bug tracking system (BTS).
+ </div>
+ </a>
+ </li>
+
+ <li class="icon_2">
+ <a href="https://stackoverflow.com/tags/frama-c/" target="_blank">
+ <div class="slideCaption">
+ Stack Overflow
+ </div>
+
+ <div class="description">
+ The Frama-C community uses Stack Overflow for general-purpose questions.
+ </div>
+ </a>
+ </li>
+
+ <li class="icon_3">
+ <a href="https://lists.gforge.inria.fr/pipermail/frama-c-discuss/" target="_blank">
+ <div class="slideCaption">
+ Frama-C-discuss
+ </div>
+
+ <div class="description">
+ The official Frama-C mailing list (announcements and general questions).
+ </div>
+ </a>
+ </li>
+
+
+ <li class="icon_4">
+ <a href="https://github.com/frama-c" target="_blank">
+ <div class="slideCaption">
+ Frama-C on Github
+ </div>
+
+ <div class="description">
+ Frama-C snapshots and related code bases (Qed, open source case studies...).
+ </div>
+ </a>
+ </li>
+
+ <li class="icon_5">
+ <a href="https://github.com/acsl-language" target="_blank">
+ <div class="slideCaption">
+ ACSL on Github
+ </div>
+
+ <div class="description">
+ Official Github repositories for the ANSI/ISO C Specification Language (ACSL).
+ </div>
+ </a>
+ </li>
+
+ <li class="icon_6">
+ <a href="/html/careers.html" target="_blank">
+ <div class="slideCaption">
+ Careers
+ </div>
+
+ <div class="description">
+ Career options at Frama-C.
+ </div>
+ </a>
+ </li>
+ </ul>
</div>
</div>
-
+
<div class="stackPost" id="stackpots">
<h3 class="subTitle">Newest Frama-C Questions & Answers on Stack Overflow</h3>
<ul id="postsStack">
-
+
</ul>
</div>
</div>
diff --git a/html/get-frama-c.html b/html/get-frama-c.html
index 6ef9c68b589f581c36be368669567f41e7115080..7e4360130df3e68798463228811dbcadd2b09c75 100755
--- a/html/get-frama-c.html
+++ b/html/get-frama-c.html
@@ -2,81 +2,81 @@
layout: default
css: get-framac
title: Get Frama-C
----
-
- <div id="wrapper" class="hfeed">
-
- {% include headers.html %}
-
- <div id="container" class="mainContainer">
- <div class="getFramaC">
- <div class="wrap">
- <h1 class="pageTitle">Choose for which terminal you want Frama C</h1>
-
- <div class="OS codeTabs">
- <a href="index.html#" role="button" data-tab="linux"><b>Linux</b></a> <a href="index.html#" role="button" data-tab=
- "mac"><b>Mac</b></a> <a href="index.html#" role="button" data-tab="windows"><b>Windows</b></a>
- </div>
-
- <div class="otherConfiguration">
- If you have a different configuration, <a target="_blank" href="https://github.com/Frama-C" class="lineMove">click
- here</a>
- </div>
-
- <div class="notebook code">
- <div>
- <div class="codeScreen">
- <div class="codeTab tab-linux hide">
- <pre style='color:#000000;background:#f9f9f9;'>opam <span style='color:#400000;'>list</span> <span style='color:#808030;'>-</span>a <span style='color:#696969;'># List the available packages</span></br>opam install lwt <span style='color:#696969;'># Install LWT</span></br>opam <span style='color:#400000;'>update</span> <span style='color:#696969;'># Update the package list...</span></br>opam upgrade <span style='color:#696969;'># Upgrade the installed packages to their latest version</span></pre>
- </div>
-
- <div class="codeTab tab-mac hide">
- <pre style='color:#000020;background:#f6f8ff;'>
-opam install depext
-opam depext frama<span style='color:#308080;'>-</span>c
-
-<span style='color:#595979;'># remove the previous version of frama-c</span>
-opam remove <span style='color:#308080;'>-</span><span style='color:#308080;'>-</span>force frama<span style=
-'color:#308080;'>-</span>c frama<span style='color:#308080;'>-</span>c<span style='color:#308080;'>-</span>base
-
-<span style='color:#595979;'># optional packages, but recommended (for efficiency, and for the GUI)</span>
-opam install depext
-opam depext zarith lablgtk conf<span style='color:#308080;'>-</span>gtksourceview conf<span style=
-'color:#308080;'>-</span>gnomecanvas
-opam install zarith lablgtk conf<span style='color:#308080;'>-</span>gtksourceview conf<span style=
-'color:#308080;'>-</span>gnomecanvas
-
-<span style='color:#595979;'># install custom version of frama-c</span>
-opam pin <span style='color:#400000;'>add</span> frama<span style='color:#308080;'>-</span>c<span style=
-'color:#308080;'>-</span>base <dir>
-</pre>
- </div>
-
- <div class="codeTab tab-windows hide">
- <pre style='color:#d1d1d1;background:#000000;'>
-<span style='color:#9999a9;'># First you need to install OPAM</span>
-opam install frama<span style='color:#d2cd86;'>-</span>c
-
-<span style='color:#9999a9;'># To get the exact list of packages</span>
-opam install depext
-opam depext frama<span style='color:#d2cd86;'>-</span>c
-
-<span style='color:#9999a9;'># optional packages, but recommended (for efficiency, and for the GUI)</span>
-opam install depext
-opam depext zarith lablgtk conf<span style='color:#d2cd86;'>-</span>gtksourceview conf<span style=
-'color:#d2cd86;'>-</span>gnomecanvas
-opam install zarith lablgtk conf<span style='color:#d2cd86;'>-</span>gtksourceview conf<span style=
-'color:#d2cd86;'>-</span>gnomecanvas
-</pre>
- </div>
- </div>
- </div>
- </div>
- </div>
+---
+
+ <div id="wrapper" class="hfeed">
+
+ {% include headers.html %}
+
+ <div id="container" class="mainContainer">
+ <div class="getFramaC">
+ <div class="wrap">
+ <h1 class="pageTitle">Choose for which OS you want Frama C</h1>
+
+ <div class="OS codeTabs">
+ <a href="index.html#" role="button" data-tab="linux"><b>Linux</b></a> <a href="index.html#" role="button" data-tab=
+ "mac"><b>Mac</b></a> <a href="index.html#" role="button" data-tab="windows"><b>Windows</b></a>
+ </div>
+
+ <div class="otherConfiguration">
+ If you have a different configuration, <a target="_blank" href="https://github.com/Frama-C" class="lineMove">click
+ here</a>
+ </div>
+
+ <div class="notebook code">
+ <div>
+ <div class="codeScreen">
+ <div class="codeTab tab-linux hide">
+ <pre style='color:#000000;background:#f9f9f9;'>opam <span style='color:#400000;'>list</span> <span style='color:#808030;'>-</span>a <span style='color:#696969;'># List the available packages</span></br>opam install lwt <span style='color:#696969;'># Install LWT</span></br>opam <span style='color:#400000;'>update</span> <span style='color:#696969;'># Update the package list...</span></br>opam upgrade <span style='color:#696969;'># Upgrade the installed packages to their latest version</span></pre>
+ </div>
+
+ <div class="codeTab tab-mac hide">
+ <pre style='color:#000020;background:#f6f8ff;'>
+opam install depext
+opam depext frama<span style='color:#308080;'>-</span>c
+
+<span style='color:#595979;'># remove the previous version of frama-c</span>
+opam remove <span style='color:#308080;'>-</span><span style='color:#308080;'>-</span>force frama<span style=
+'color:#308080;'>-</span>c frama<span style='color:#308080;'>-</span>c<span style='color:#308080;'>-</span>base
+
+<span style='color:#595979;'># optional packages, but recommended (for efficiency, and for the GUI)</span>
+opam install depext
+opam depext zarith lablgtk conf<span style='color:#308080;'>-</span>gtksourceview conf<span style=
+'color:#308080;'>-</span>gnomecanvas
+opam install zarith lablgtk conf<span style='color:#308080;'>-</span>gtksourceview conf<span style=
+'color:#308080;'>-</span>gnomecanvas
+
+<span style='color:#595979;'># install custom version of frama-c</span>
+opam pin <span style='color:#400000;'>add</span> frama<span style='color:#308080;'>-</span>c<span style=
+'color:#308080;'>-</span>base <dir>
+</pre>
+ </div>
+
+ <div class="codeTab tab-windows hide">
+ <pre style='color:#d1d1d1;background:#000000;'>
+<span style='color:#9999a9;'># First you need to install OPAM</span>
+opam install frama<span style='color:#d2cd86;'>-</span>c
+
+<span style='color:#9999a9;'># To get the exact list of packages</span>
+opam install depext
+opam depext frama<span style='color:#d2cd86;'>-</span>c
+
+<span style='color:#9999a9;'># optional packages, but recommended (for efficiency, and for the GUI)</span>
+opam install depext
+opam depext zarith lablgtk conf<span style='color:#d2cd86;'>-</span>gtksourceview conf<span style=
+'color:#d2cd86;'>-</span>gnomecanvas
+opam install zarith lablgtk conf<span style='color:#d2cd86;'>-</span>gtksourceview conf<span style=
+'color:#d2cd86;'>-</span>gnomecanvas
+</pre>
+ </div>
+ </div>
+ </div>
+ </div>
+ </div>
</div>
-
- {% include footer.html %}
-
- <div class="clear"></div>
- </div>
- </div>
+
+ {% include footer.html %}
+
+ <div class="clear"></div>
+ </div>
+ </div>
diff --git a/html/kernel.html b/html/kernel.html
index 72e609c5e20e2724f08843650b14e74fd4eb97f0..42061efa3b5684b7c288149d506ba50b931cbca1 100755
--- a/html/kernel.html
+++ b/html/kernel.html
@@ -3,159 +3,169 @@ layout: default
css: plugin
title: Kernel & Plugins - Frama-C
---
-
-<body class="page-template page-template-page-kernel page-template-page-kernel-php page page-id-179 nonTouch">
- <div id="wrapper" class="hfeed">
-
-
- {% include headers.html %}
-
- <div id="container" class="mainContainer">
- <div class="tabs">
- <div class="wrap">
- <a class="tabLink" href="/html/kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink active" href=
- "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/gui.html">GUI</a>
- </div>
- </div>
-
- <div class="pageKernel pages">
- <div class="bgTextbig">
- Kernel
- </div>
-
- <div class="wrap">
- <p>WIP (TA)</p>
-
- <p>The Frama-C kernel acts as a <em>lingua franca</em> for all <a href=
- "https://framac-staging.eu-staging.kacdn.net/kernel-plugin/">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>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
- 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>• 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>
-
- <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>
- 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. 3.3. Projects 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. 3.4. Collaborations across analyzers 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: • 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
- 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>
-
+
+<body class="page-template page-template-page-kernel page-template-page-kernel-php page page-id-179 nonTouch">
+ <div id="wrapper" class="hfeed">
+
+
+ {% include headers.html %}
+
+ <div id="container" class="mainContainer">
+ <div class="tabs">
+ <div class="wrap">
+ <a class="tabLink" href="/html/kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink active" href=
+ "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/gui.html">GUI</a>
+ </div>
+ </div>
+
+ <div class="pageKernel pages">
+ <div class="bgTextbig">
+ Kernel
+ </div>
+
+ <div class="wrap">
+ <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>
+
+ <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>
+
+ <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>
+
+ <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>
+
+ <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>
+
+ <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>
+
<div class="aboutKernel">
- <h2 class="subTitle">Some articles about kernal sections</h2>
+ <h2 class="subTitle">Some articles about kernel sections</h2>
<div class="kernelSwiper swiper-container">
<div class="swiper-wrapper">
@@ -217,12 +227,12 @@ title: Kernel & Plugins - Frama-C
<div class="swiper-pagination"></div>
</div>
- </div>
- </div>
+ </div>
+ </div>
</div>
- {% include footer.html %}
-
- <div class="clear"></div>
- </div>
- </div>
-</body>
\ No newline at end of file
+ {% include footer.html %}
+
+ <div class="clear"></div>
+ </div>
+ </div>
+</body>
diff --git a/html/terms-of-use.html b/html/terms-of-use.html
index 9949e4f03f081efa5a2a42b27cb6f5559f54804d..2e656e6874513735b3bd7728808b16f3ef9c098f 100755
--- a/html/terms-of-use.html
+++ b/html/terms-of-use.html
@@ -1,64 +1,64 @@
---
layout: default
css: terms
----
-
-<div id="wrapper" class="hfeed">
+---
+
+<div id="wrapper" class="hfeed">
+
+{% include headers.html %}
+
+<div id="container" class="mainContainer">
+ <div class="pages pageTerms">
+ <dl class="defnitionList">
+ <dt class="subTitle">Legal information and diffusion rights</dt>
+
+ <dd>
+ <p>All materials and graphical elements contained on this site are protected by French and international copyright law
+ and intellectual property rights. Reproduction in part or in whole of materials and graphical elements of this site is
+ prohibited without the express permission of the Director of publication.</p>
+ </dd>
+
+ <dt class="subTitle">Contacts</dt>
+
+ <dd>
+ <p>For requests to use any of the contents of this site, please contact us:</p>
-{% include headers.html %}
-
-<div id="container" class="mainContainer">
- <div class="pages pageTerms">
- <dl class="defnitionList">
- <dt class="subTitle">Legal information and diffusion rights</dt>
-
- <dd>
- <p>All materials and graphical elements contained on this site are protected by French and international copyright law
- and intellectual property rights. Reproduction in part or in whole of materials and graphical elements of this site is
- prohibited without the express permission of the Director of publication.</p>
- </dd>
-
- <dt class="subTitle">Contacts</dt>
-
- <dd>
- <p>For requests to use any of the contents of this site, please contact us:</p>
-
- <div>
- <h5>Director of publication</h5>
-
- <p>C. Marché<br>
- INRIA - 4, rue Jacques Monod<br>
- F-91893 Orsay cedex</p>
- </div>
-
- <div>
- <h5>Webmaster</h5>
-
- <p>Florent.Kirchner@cea.fr<br>
- F. Kirchner<br>
- CEA Saclay<br>
- F-91191 Gif sur Yvette cedex</p>
- </div>
- </dd>
-
- <dt class="subTitle">Déclaration CNIL</dt>
-
- <dd>
- <p>Conformément à la loi n° 78-17 du 6 janvier 1978, relative à l'Informatique, aux Fichiers et aux Libertés, vous
- disposez d'un droit d'accès et de rectification des informations nominatives vous concernant. Vous pouvez l'exercer en
- vous adressant à :</p>
-
- <div>
- Florent.Kirchner@cea.fr<br>
- F. Kirchner<br>
- CEA Saclay<br>
- F91191 Gif sur Yvette cedex
- </div>
- </dd>
- </dl>
+ <div>
+ <h5>Director of publication</h5>
+
+ <p>C. Marché<br>
+ Inria - 4, rue Jacques Monod<br>
+ F-91893 Orsay cedex</p>
+ </div>
+
+ <div>
+ <h5>Webmaster</h5>
+
+ <p><a href="mailto:florent.kirchner@cea.fr">florent.kirchner(at)cea.fr</a><br>
+ F. Kirchner<br>
+ CEA Saclay<br>
+ F-91191 Gif sur Yvette cedex</p>
+ </div>
+ </dd>
+
+ <dt class="subTitle">Déclaration CNIL</dt>
+
+ <dd>
+ <p>Conformément à la loi n° 78-17 du 6 janvier 1978, relative à l'Informatique, aux Fichiers et aux Libertés, vous
+ disposez d'un droit d'accès et de rectification des informations nominatives vous concernant. Vous pouvez l'exercer en
+ vous adressant à :</p>
+
+ <div>
+ <a href="mailto:florent.kirchner@cea.fr">florent.kirchner(at)cea.fr</a><br>
+ F. Kirchner<br>
+ CEA Saclay<br>
+ F-91191 Gif sur Yvette cedex
+ </div>
+ </dd>
+ </dl>
</div>
- {% include footer.html %}
-
- <div class="clear"></div>
-</div>
-</div>
+ {% include footer.html %}
+
+ <div class="clear"></div>
+</div>
+</div>
diff --git a/html/using-frama-c.html b/html/using-frama-c.html
index a8c57222065e5bbd0de6508190e0961c4527d817..9901cb57ac4a788a6d875fae7e210962cbfd3729 100755
--- a/html/using-frama-c.html
+++ b/html/using-frama-c.html
@@ -1,12 +1,12 @@
---
-layout: default
+layout: default
title: Using Frama C - Frama-C
css: plugin
---
<body class="page-template page-template-page-usingFramac page-template-page-usingFramac-php page page-id-12 nonTouch">
<div id="wrapper" class="hfeed">
-
+
{% include headers.html header=1 %}
<div id="container" class="mainContainer">
@@ -29,8 +29,7 @@ css: plugin
<p>The C language has been in use for a long time, and numerous programs today make use of C routines. This
ubiquity is due to historical reasons, and to the fact that C is well adapted for a significant number of
- applications (e.g. embedded code). However, the C language exposes many notoriously awkward constructs. precise
- analyses despite the pitfalls of C</p>
+ applications (e.g. embedded code). However, the C language exposes many notoriously awkward constructs.</p>
<p><b>Many Frama-C plug-ins are able to reveal what the analyzed C code actually does. Equipped with Frama-C, you
can:</b></p>
@@ -108,7 +107,7 @@ css: plugin
<div id="group_security_defects">
<div class="paragraphGroup">
- <h3>Detect Security Defects</h3>
+ <h3>Detect security defects</h3>
<p>Frama-C allows to verify that the source code complies with a provided formal specification. Functional
specifications can be written in a dedicated language, ACSL. The specifications can be partial, concentrating
@@ -167,7 +166,7 @@ css: plugin
</div>
</section>
</div>
-
+
{% include footer.html %}
<div class="clear"></div>
diff --git a/index.html b/index.html
index 44bde55f238d4e74338c840f521e28f46e37287e..b27e400bd5dd2a2d1cb059f9c324bbbe39777741 100755
--- a/index.html
+++ b/index.html
@@ -6,7 +6,7 @@ title: Frama-C
<body class="home page-template-default page page-id-7 nonTouch">
<div id="wrapper" class="hfeed">
-
+
{% include headers.html %}
<div id="container" class="mainContainer">
@@ -82,7 +82,7 @@ title: Frama-C
</div>
<div class="title">
- <b>02</b><span>Option <samp>-val</samp> runs the Evolved Value Analysis plug-in and prepares its
+ <b>02</b><span>Option <samp>-eva</samp> runs the Eva plug-in and prepares its
results.</span>
</div>
@@ -230,7 +230,7 @@ value analysis.</span></span></span></span></span>
<span style="color: #d0d0d0">}</span>
<span style="color: #6ab825; font-weight: bold">return</span> <span style="color: #d0d0d0">S;</span>
<span style="color: #d0d0d0">}</span>
-
+
<span class="highlight">*tmp = S;</span> <span style="color: #d0d0d0">modifies</span> <span style=
"color: #d0d0d0">T[</span><span style="color: #3677a9">0..4</span><span style="color: #d0d0d0">]</span><span class=
"arrowTooltip right"><span><span class=
@@ -447,7 +447,7 @@ value analysis.</span></span></span></span></span>
<div id="download_iv_point" class="inviewCenter"></div>
</section>
-
+
{% include footer.html %}
<section class="bgTitleBlk titleIn white">