Merge branch 'master' of git.frama-c.com:frama-c/frama-c.frama-c.com

dokuwiki/external_plugins.md

----
-layout: clean_page
----
+---
+layout: clean_page
+---
 # External plug-ins
 
 This is a list of plug-ins that you may find useful but are not
@@ -12,6 +12,27 @@ luck on the mailing list.
 Add your own plug-in if you think it can be useful to other and want to
 share it with the world\!
 
+## Pilat
+
+URL: <http://steven-de-oliveira.fr/index.php?page=tool_pilat>
+
+PILAT (for Polynomial Invariants by Linear Algebra Tool) is an invariant
+generator based on the study of matrices. It processes loops with polynomial
+assignments and linearize them, then searches for left eigenvectors of the
+resulting matrix. Those vectors expresses invariants of the loop.
+
+## StaDy
+
+URL: <https://github.com/gpetiot/Frama-C-StaDy>
+
+StaDy is an integration of the concolic test generator PathCrawler within
+the software analysis platform Frama- C. When executing a dynamic analysis
+of a C code, the integrated test generator also exploits its formal specification,
+written in an executable fragment of the acsl specification language shared
+with other analyzers of Frama-C. The test generator provides the user with
+accurate verdicts, that other Frama-C plugins can reuse to improve their own
+analyses.
+
 ## Jessie
 
 URL: <http://krakatoa.lri.fr/>
@@ -30,7 +51,7 @@ asked about it have been gathered on their [own page](/dokuwiki/jessie.html), or
 
 ## Celia
 
-URL: <http://www.liafa.univ-paris-diderot.fr/celia/>
+URL: <https://www.irif.fr/~sighirea/celia/>
 
 CELIA is a tool for the static analysis and verification of C programs
 manipulating dynamic (singly linked) lists. The static analyser computes

dokuwiki/faq.md

----
-layout: clean_page
----
-# Tips and Frequently asked questions
-
-### Frequently Asked in frama-c-discuss
-
-Éric Jenn has compiled a list of [Frequently Asked Questions](/dokuwiki/frequently_asked_questions.html) and answers based on
-contributions to the
-[frama-c-discuss](/mailto/frama-c-discuss@lists.gforge.inria.fr) list.
-
-# Parsing
-
-### Pre-processing the annotations
-
-By default, the preprocessor does not process comments. ACSL
-annotations, unfortunately, look like comments to the preprocessor. If
-you use the GCC preprocessor (also known as GNU CPP), you can force the
-preprocessing of annotations with the `-pp-annot` option.
-
-    frama-c -pp-annot [other options]
-
-### Using standard headers
-
-Since Frama-C Boron, a large part of the C99 standard library headers
-are installed with Frama-C, in the `${FRAMAC_SHARE}/libc` directory. It
-is better to use these headers rather than the ones that might be
-present on your system, as they contain some specific information that
-will help the analyses, such as in particular ACSL specifications for
-some of the functions. In order to `#include` such an header file, you
-can use *e.g.* the following command:  
-``frama-c -cpp-extra-args="-I`frama-c -print-path`/libc" [other
-options]``
-
-### Booleans
-
-The C99 type `bool` is not automatically supported by Frama-C. To use
-`bool` in your code, add this line:
-
-    typedef enum _bool { false = 0, true = 1 } bool ;
-
-Note that C99 uses a pre-defined type `_Bool` (see paragraph 6.2.5),
-that is supported by Frama-C. The standard library defines a **macro**
-`bool` (that expands to `_Bool`) in `stdbool.h`.
-
-### What do I need to be able to use the Windows Frama-C package?
-
-You need to install a C preprocessor. Any preprocessor can be used, but
-the best preprocessor to choose is the one that is supposed to be used
-to preprocess the application you want to analyze.
-
-If you just seek any C preprocessor for testing purpose, you may want to
-install Cygwin and add the gcc development package or any version you
-can find on the web. Page 40 of the Value analysis manual gives hints
-for other preprocessors (MSVC):
-
-    frama-c-gui -cpp-command ’gcc -C -E -I . -x c ’
-    frama-c-gui -cpp-command ’gcc -C -E -I . -o %2 %1'
-    frama-c-gui -cpp-command ’copy %1 %2’
-    frama-c-gui -cpp-command ’cat %1 > %2’
-    frama-c-gui -cpp-command ’CL.exe /C /E %1 > %2’
-
-# Jessie and WP
-
-### Installing theorem provers
-
-Links for installing provers are provided on [Why3's
-page](http://why3.lri.fr/#provers).  
-Here are detailed instructions for making use of Z3:
-
-  - go to [Z3 source
-    homepage](http://z3.codeplex.com/SourceControl/latest#README)
-  - Click on the 'Download' button
-  - Save the zip in a local folder, say z3-sources/.
-  - Run the following commands:
-
-<!-- end list -->
-
-    cd z3-sources
-    unzip z3[tab for completion]
-    cd z3[tab for completion]
-    autoconf
-    ./configure
-    python scripts/mk_make.py
-    cd build
-    make
-    sudo make install
-
-  - z3 executable is installed at /usr/bin, libraries at /usr/lib, and
-    include files at /usr/include.
-  - Run `why3config --detect` (the provers, the versions and the plugins
-    detected can be differrent)
-
-<!-- end list -->
-
-    Found prover Alt-Ergo version 0.95.1, Ok.
-    Found prover CVC3 version 2.4.1, Ok.
-    Found prover Spass version 3.7, Ok.
-    Found prover Z3 version 4.3.1, Ok.
-    Found prover Coq version 8.4pl1, Ok.
-    Warning: prover Gappa version 0.17.1 is not known to be supported, use it at your own risk!
-    5 provers detected and 1 provers detected with unsupported version
-    == Found [..]/why3/lib/why3/plugins/hypothesis_selection.cmxs ==
-    == Found [..]/why3/lib/why3/plugins/tptp.cmxs ==
-    == Found [..]/why3/lib/why3/plugins/dimacs.cmxs ==
-    == Found [..]/why3/lib/why3/plugins/genequlin.cmxs ==
-    Save config to ~/.why3.conf
-
-### Jessie specific questions
-
-See [Jessie's page](/dokuwiki/jessie.html).
-
-# Graphical user interface
-
-### Is there an Eclipse plug-in?
-
- 
-  * An Eclipse plug-in providing equivalent functionality to gWhy (for Weakest Precondition plug-ins) is currently maintained by Nickolay V. Shmyrev and [[http://github.com/frama-c-eclipse/frama-c-eclipse|is available on GitHub]]. This plug-in works on Linux, but not yet on Windows.
-  * (fcdt)[http://gforge.enseeiht.fr/projects/fcdt/|fcdt] is another Eclipse plug-in, that allows to use value analysis from Eclipse
-
-
-### How do I customize the GUI?
-
-Starting with 20090901 (Beryllium), you can create a file named
-frama-c-user.rc in $FRAMAC\_SHARE. An example of the syntax to use can
-be found in the file $FRAMAC\_SHARE/frama-c.rc.
-
-# Misc
-
-### Validity of memory zones
-
-ACSL (hence Frama-C) uses a typed memory model. That is, each block of
-allocated memory is associated with a type. These can be simple types,
-such as char or int, as well as structs. Therefore, the code below is
-correct
-
-    struct A {
-        int x;
-        int y;
-    };
-    struct B {
-        struct A a;
-        int z;
-    };
-    
-    /*@ requires \valid(p);
-     */
-    void foo(struct B *p) {
-      p->a.x = 0;
-      p->z = 0;
-    }
-
-Note however that arrays are considered as chunks of data of the same
-type. Therefore, this example does not verify:
-
-    typedef int arr3[3];
-    
-    /*@ requires \valid(a);
-     */
-    foo(arr3 a) {
-      a[2] = 0;
-    }
-
-Instead, the correct annotation is
-
-    typedef int arr3[3];
-    
-    /*@ requires \valid(a+ (0..2));
-     */
-    foo(arr3 a) {
-      a[2] = 0;
-    }
-
-### Checking the alignment of some memory accesses with the value analysis
-
-It is possible to check explicitly that a few memory accesses are
-aligned with the value analysis. Check the [Explicit alignment
-howto](Explicit%20alignment%20howto).

dokuwiki/start.md

@@ -2,6 +2,7 @@
 layout: clean_page
 title: Documentation
 ---
+
 # Documentation
 
 <!-- Is on-topic in this wiki anything that may be of help to others users of -->
@@ -17,7 +18,7 @@ submitting a merge requests at the corresponding
 [https://git.frama-c.com/frama-c/frama-c.frama-c.com](gitlab repository).
 
 For plug-ins documentation, some pages can be found here but all of them are
-otherwise available [/html/kernel-plugin.html](on the dedicated page).
+otherwise available [on the dedicated page](/html/kernel-plugin.html).
 
 Is on-topic anything that may be of help to others users of
 Frama-C and related tools: tips, changes that you have noticed,
@@ -29,49 +30,73 @@ workarounds, etc.
 <!-- functional that it puts the authors of Frama-C's various manuals to -->
 <!-- shame. -->
 
------
+-------
 
 # Compilation and Installation
 
-Current and old releases of Frama-C are available on [this
-page](html/get-frama-c.html). It contains the official
-installation instructions for supported systems.
+Current and old releases of Frama-C are available on [this page](html/get-frama-c.html).
+It contains the official installation instructions for supported systems.
 
-Otherwise, [each releases](https://git.frama-c.com/pub/frama-c/blob/master/INSTALL.md) contains extra instructions
-for compiling from source.
+Otherwise, [each releases](https://git.frama-c.com/pub/frama-c/blob/master/INSTALL.md)
+contains extra instructions for compiling from source.
 
 <!-- We could copy INSTALL.md to this repo -->
 
-# Contributing
+-----
 
-Frama-C is an open-source project which could be contrinuted through merge
-requests at this [Gitlab repository](https://git.frama-c.com/pub/frama-c/). The
-modalities are described in this [document](https://git.frama-c.com/pub/frama-c/CONTRIBUTING.md)
+# Manuals and tutorials
 
-<!-- We could copy CONTRIBUTING.md to this repo -->
+### ACSL
+
+- [Description](/html/acsl.html)
+- [Manual](/download/acsl.pdf)
+- [Online](/html/acsl_tutorial_index.html) and [PDF](/download/acsl-tutorial.pdf) tutorial
+
+### Frama-C
+
+- [Description](/html/kernel.html)
+- [Manual](/download/frama-c-user-manual.pdf)
+- [ACSL implementation](/download/frama-c-acsl-implementation.pdf)
 
-# FAQ, Tips and Tricks
+### Plugins
 
-See [this page](/dokuwiki/faq.html), or this [slightly older
-one](/dokuwiki/frequently_asked_questions.html).
+- Eva [Description](/fc-plugins/eva.html) - [Manual and tutorial](/download/frama-c-eva-manual.pdf)
+- WP [Description](/fc-plugins/wp.html) - [Manual](/download/frama-c-wp-manual.pdf)
+- E-ACSL [Description](/fc-plugins/e-acsl.html) - [Manual](/download/e-acsl/e-acsl-manual.pdf)
+- RTE [Description](/fc-plugins/rte.html) - [Manual](/download/frama-c-rte-manual.pdf)
+- Aoraï [Description](/fc-plugins/aorai.html) - [Manual](/download/frama-c-aorai-manual.pdf)
+- Metrics [Description](/fc-plugins/metrics.html)
+- Occurrences analysis [Description](/fc-plugins/occurrence.html)
+- Scope analysis [Description](/fc-plugins/scope.html)
+- Slicing [Description](/fc-plugins/slicing.html)
+- Semantic constant folding [Description](/fc-plugins/semantic-constant-folding.html)
+- Spare code elimination [Description](/fc-plugins/spare-code.html)
+- Impact analysis [Description](/fc-plugins/impact.html)
 
-# External plug-ins
+### Plugin development
+
+- [Manual](/download/frama-c-plugin-development-guide.pdf)
+
+### External plug-ins
 
 [External plug-ins](/dokuwiki/external_plugins.html) that you may find
 useful are available. The plug-ins currently described are **Jessie**,
 **Celia** and **Werror**.
 
-# Known issues
+------
 
-  - The BTS has a [list of known
-    issues](http://bts.frama-c.com/view_all_bug_page.php).
-  - See [bug reporting guidelines](/dokuwiki/bug_reporting_guidelines.html) to
-    report a bug.
+# Contributing
 
-# Open positions
+Frama-C is an open-source project which could be contrinuted through merge
+requests at this [Gitlab repository](https://git.frama-c.com/pub/frama-c/). The
+modalities are described in this [document](https://git.frama-c.com/pub/frama-c/CONTRIBUTING.md)
+
+<!-- We could copy CONTRIBUTING.md to this repo -->
+
+# Known issues
 
-[Open positions](/dokuwiki/positions.html) in the Frama-C team are
-available.
+  - The BTS has a [list of known issues](http://bts.frama-c.com/view_all_bug_page.php).
+  - See [bug reporting guidelines](/dokuwiki/bug_reporting_guidelines.html) to report a bug.
 
 # Works about Frama-C
 

dokuwiki/teaching.md

----
-layout: clean_page
----
+---
+layout: clean_page
+---
 # Frama-C in teaching
 
 This page lists various courses that are using Frama-C in their lab
@@ -8,8 +8,6 @@ lessons.
 
 ## In English
 
-  - [University of Iowa: Formal Methods in Software
-    Engineering](http://homepage.divms.uiowa.edu/~pgaroche/181/syllabus.shtml)
   - [University of Minho: Formal Methods in Software
     Engineering](http://mei.di.uminho.pt/?q=en/1112/mfes-uk)
   - [University College London: Language-based
@@ -20,12 +18,8 @@ lessons.
   - [ENSIIE Evry: Static Analysis of Programs](/dokuwiki/ensiie.html)
   - [École Polytechnique: Initiation to Program
     Proof](http://www.enseignement.polytechnique.fr/profs/informatique/Sylvie.Putot/Enseignement/SemantiqueValidation/TP6.html)
-  - [ENSI Bourges: Specification and Test of
-    Applications](http://enseignement.ensi-bourges.fr/ects/modules/fiche.php?id=2513&lang=fr)
 
 ## In other languages
 
-  - [Humboldt University Berlin: Deductive Verification (in
-    German)](http://www2.informatik.hu-berlin.de/~hs/Lehre/2011-WS_SWV1/index.html)
   - [Moscow State University: Formal Specification and Verification (in
     Russian)](http://sed.ispras.ru/fmprac)

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>

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>

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>

html/get-frama-c.html

@@ -2,82 +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 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
 
-			<a href="/html/framac-versions.html" class="previousVersion">Previous Versions</a>
-          <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 &lt;dir&gt;
-</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>
+<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 &lt;dir&gt;
+</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>

html/terms-of-use.html

 ---
 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>

html/using-frama-c.html

 ---
-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>

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=
@@ -385,7 +385,7 @@ value analysis.</span></span></span></span></span>
 
             <div id="event_detail_swiper" class="eventDetailsBlock swiper-container">
               <div class="swiper-wrapper">
-			    {% for event in site.events %}
+			    {% for event in site.events reversed %}
                 <div class="swiper-slide">
                   <div class="eventDetail" id="post_details_486">
                     <figure>
@@ -398,8 +398,7 @@ value analysis.</span></span></span></span></span>
 					  <div>
                         <h3>{{ event.title }}</h3>
 
-                        <p>{{ event.content | strip_html | truncatewords: 50 }}</p><a class="read-more link" href=
-                        "{{ event.url }}" target="_blank">Read More</a>
+                        <p>{{ event.content }}</p>
                       </div>
                     </div>
                   </div>
@@ -416,7 +415,7 @@ value analysis.</span></span></span></span></span>
 
             <div id="event_calender_swiper" class="swiper-container">
               <div class="swiper-wrapper">
-			    {% for event in site.events %}
+			    {% for event in site.events reversed %}
                 <div class="swiper-slide">
                   <a role="button" class="eventLink"><time>{{ event.date | date: "<b>%-d</b><small>%B</small>" }}</time><span>{{ event.title }}</span></a>
                 </div>
@@ -448,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">
@@ -472,4 +471,4 @@ value analysis.</span></span></span></span></span>
       <div class="clear"></div>
     </div>
   </div>
-<body>
+<body>
\ No newline at end of file