Compare revisions

3b633685 · 3b633685 · 3b633685 · 3b633685 · 3b633685 · 3b633685
--- a/_events/framac-18.0.md
+++ b/_events/framac-18.0.md
 ---
 layout: default
 date: 29-10-2018
+event: Frama-C 18.0 (Argon)
 title: Release of Frama-C 18.0 (Argon)
-image: /assets/img/events/Argon.jpg
 ---
 Frama-C 18.0 (Argon) is out. Download it [here](/fc-versions/argon.html).
\ No newline at end of file
+Main changes with respect to Frama-C 17 (Chlorine) include:
+#### Kernel:
+- Improved command-line options for treatment of warning categories:
+  -plugin-warn-key category:status will set the status of category,
+  instead of using 7 options -plugin-warn-abort, -plugin-warn-feedback, …
+  with awkward ± categories
+- All errors emitted during a run will now lead to a non-zero exit status
+  of frama-c command line
+- options for emitting an alarm on [left|right] shift of a negative
+  value are now at kernel level (and removed from Eva)
+- const globals are now unconditionally constants (option -const-writable is
+  removed)
+- several improvements to the frama-c libc specifications
+- new binary frama-c-script to help with case studies
+#### Eva:
+- Eva is now consistently named "Eva", and all its options start with -eva
+  (compatibility with previous option names has been preserved).
+- New "//@ loop unroll N;" annotations to unroll exactly the N first iterations
+  of a loop, as an improvement over slevel options.
+- The memexec cache is compatible with all domains, and is enabled by default.
+  This cache greatly improves the analysis time.
+- Builtins for memset and memcpy are now included in the open-source release.
+- Alternative domains use the frama-c libc specification when a builtin is used,
+  to minimize the loss of precision.
+- Emits alarms when reading trap representations of type _Bool.
+- New experimental domain numerors inferring absolute and relative errors of
+  floating-point computations. Does not handle loops for now.
+#### E-ACSL:
+- support of ranges in memory built-ins, e.g. \valid(t+(0..9))
+- support of \at on logic variables, e.g. \forall integer i; 0 <= i < 10 ==> t[i] == \old(t[i])
+A complete Changelog can be found [here](/html/changelog.html#Argon-18.0).
\ No newline at end of file
--- a/_events/framac-19.0.md
+++ b/_events/framac-19.0.md
 ---
 layout: default
 date: 21-06-2019
+event: Frama-C 19.0 (Potassium)
 title: Release of Frama-C 19.0 (Potassium)
-image: /assets/img/events/Potassium.jpg
 ---
 Frama-C 19.0 (Potassium) is out. Download it [here](/fc-versions/potassium.html).
\ No newline at end of file
+Main changes with respect to Frama-C 18 (Argon) include:
+#### Kernel:
+- new check annotation, similar to assert except that it does not introduce
+  additional hypotheses on the program state
+- new options added to frama-c-script
+#### GUI:
+- compatibility with lablgtk3
+#### Eva:
+- New annotation "//@ split exp" to separate the analysis states for each
+  possible value of an expression until a "//@ merge exp" annotation.
+- New option -eva-partition-history to delay the join of the analysis states at
+  merging points; useful when a reasoning depends on the path taken to reach a
+  control point.
+- By default, prints a summary at the end of the analysis.
+- New meta option -eva-precision to globally configure the analysis.
+- Improved precision on nested loops.
+#### WP:
+- new auto-search mode to automatically apply strategies and tactics (see -wp-auto)
+- extended simplifications on range, bitwise and C-boolean values (_Bool is now
+  handled by default)
+- refactored float model (although it still requires further axiomatisation)
+#### E-ACSL:
+- support for user-defined logic functions and predicates without labels
+- new option -e-acsl-functions that allows the user to specify a white/black list
+  of functions in which annotations are monitored, or not.
+A complete changelog can be found [here](/html/changelog.html#Potassium-19.0).
\ No newline at end of file
--- a/_events/framac-19.1.md
+++ b/_events/framac-19.1.md
 ---
 layout: default
 date: 17-09-2019
+event: Frama-C 19.1
 title: Release of Frama-C 19.1 (Potassium)
-image: /assets/img/events/Potassium.jpg
 ---
 Frama-C 19.1 (Potassium) is out. Download it [here](/fc-versions/potassium.html).
\ No newline at end of file
+This minor release merely restores compatibility with OCaml 4.08.1 (and the new
+4.09.0), and fixes a few issues with lablgtk3.
\ No newline at end of file
--- a/_events/framac-20.0.md
+++ b/_events/framac-20.0.md
+---
+layout: default
+date: 04-12-2019
+event: Frama-C 20.0 (Calcium)
+title: Release of Frama-C 20.0 (Calcium)
+---
+Frama-C 20.0 (Calcium) is out. Download it [here](/fc-versions/calcium.html).
+Main changes with respect to Frama-C 19 (Potassium) include:
+#### Kernel:
+  - the minimum required OCaml version is now 4.05.0
+  - more strict checks related to ghost variables in non-ghost code, and support for ghost parameters
+  - visitor behavior functions were moved from Cil to a new module Visitor_behavior
+#### Eva:
+  - New octagon domain inferring relations of the form
+  a ≤ ±X±Y ≤ b between pairs of integer variables X and Y.
+  - New option "-eva-auto-loop-unroll N", to unroll all
+  loops whose number of iterations can be easily bounded by <N>.
+  - Dynamic registration of abstract values and domains:
+  developers of new domains no longer need to modify Eva's engine.
+#### WP:
+- Use native Why3 API (now requires why3 at compile time); deprecated native alt-ergo & coq output
+- New cache mechanism for why3 provers, see -wp-cache option
+#### E-ACSL:
+- Support of rational numbers and operations.
+And a new plug-in, Markdown-report (MdR), to generate reports in both Markdown and SARIF formats.
+A complete changelog can be found [here](/html/changelog.html#Calcium-20.0).
\ No newline at end of file
--- a/_includes/headers.html
+++ b/_includes/headers.html
 <header class="siteHeader" id="site_header">
-  <div id="header_iv_point" class="inviewTop"></div><span class="brandLogo"><a href="/index.html" rel="home" title=
+  <div id="header_iv_point" class="inviewTop"></div>
+  <span class="brandLogo"><a href="/index.html" rel="home" title=
  "Frama-C"><img src="/assets/img/framac.gif" alt=""><span>Frama-C</span></a></span><a role="button" id=
  "menu_toggle" class="menuToggle"><span class="open"><i></i><i></i><i></i></span><span class="close"><i></i><i></i></span></a>
  <nav id="menu" role="navigation">
 	<div class="menu-primary-meny-container">
 	  <ul id="menu-primary-meny" class="menu">
-		{% if include.header != null and include.header == 1 %}
+	  {% for item in site.data.nav %}
-		<li id="menu-item-25" class=
+	  {% if forloop.index == include.header %}
-		"menu-item menu-item-type-post_type menu-item-object-page current-menu-item page_item page-item-12 current_page_item menu-item-25">
+	  <li class="menu-item menu-item-type-post_type menu-item-object-page current-menu-item page_item current_page_item">
-		{% else %}
+	  {% else %}	  
-		<li id="menu-item-25" class="menu-item menu-item-type-post_type menu-item-object-page menu-item-25">		
+	  <li class="menu-item menu-item-type-post_type menu-item-object-page">		
-		{% endif %}
+	  {% endif %}
-		  <a href="/html/using-frama-c.html">Using Frama-C</a>
+	    <a href="{{ item.link }}">{{ item.name }}</a>
-		</li>
+	  </li>
+	  {% endfor %}
-		{% if include.header != null and include.header == 2 %}
-        <li id="menu-item-26" class=
-		"menu-item menu-item-type-post_type menu-item-object-page current-menu-item page_item page-item-16 current_page_item menu-item-26">
-		{% else %}
-		<li id="menu-item-26" class="menu-item menu-item-type-post_type menu-item-object-page menu-item-26">		
-		{% endif %}
-		  <a href="/html/kernel-plugin.html">Features</a>
-		</li>
-		{% if include.header != null and include.header == 4 %}
-		<li id="menu-item-28" class=
-		"menu-item menu-item-type-post_type menu-item-object-page current-menu-item page_item page-item-20 current_page_item menu-item-28">
-		{% else %}
-		<li id="menu-item-28" class="menu-item menu-item-type-post_type menu-item-object-page menu-item-28">
-		{% endif %}
-		<a href="/dokuwiki/start.html">Documentation</a>
-		</li>
-		{% if include.header != null and include.header == 5 %}
-		<li id="menu-item-29" class=
-		"menu-item menu-item-type-post_type menu-item-object-page current-menu-item page_item page-item-22 current_page_item menu-item-29">
-		{% else %}
-		<li id="menu-item-29" class="menu-item menu-item-type-post_type menu-item-object-page menu-item-29">		
-		{% endif %}
-		  <a href="/blog/index.html">Blog</a>
-		</li>
-		{% if include.header != null and include.header == 6 %}
-		<li id="menu-item-30" class=
-		"menu-item menu-item-type-post_type menu-item-object-page current-menu-item page_item page-item-22 current_page_item menu-item-30">
-		{% else %}
-		<li id="menu-item-30" class="menu-item menu-item-type-post_type menu-item-object-page menu-item-30">		
-		{% endif %}
-		  <a href="/html/careers.html">Careers</a>
-		</li>
-		{% if include.header != null and include.header == 3 %}
-		<li id="menu-item-27" class=
-		"menu-item menu-item-type-post_type menu-item-object-page current-menu-item page_item page-item-18 current_page_item menu-item-27">
-		{% else %}
-		<li id="menu-item-27" class="menu-item menu-item-type-post_type menu-item-object-page menu-item-27">		
-		{% endif %}
-		  <a href="/html/contact.html">Contact</a>
-		</li>
 	  </ul>
-	</div><a role="button" href="/html/get-frama-c.html" id="header_download_link" class="btnDownload"><span><i class=
+	</div>
+	<a role="button" href="/html/get-frama-c.html" id="header_download_link" class="btnDownload"><span><i class=
 	"icon icon-curly-left"></i><i class="icon icon-download-arrow"></i><i class="icon icon-curly-right"></i></span></a>
  </nav>
 </header>
--- a/_layouts/blog.html
+++ b/_layouts/blog.html
@@ -6,7 +6,7 @@ css: blog
 <div id="wrapper" class="hfeed">
-	{% include headers.html header=5 title=Blog %}
+	{% include headers.html header=4 title=Blog %}
 <div id="container" class="mainContainer">
  <div class="defaultPage blogsPage" id="content" role="main">

--- a/_layouts/clean_page.html
+++ b/_layouts/clean_page.html
@@ -6,7 +6,7 @@ css: wiki
 <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 header=4%}
+{% include headers.html header=3 %}
 <div id="container" class="mainContainer">
  <div class="defaultPage wikiPage pages textLeft" id="content" role="main">

--- a/_layouts/feature.html
+++ b/_layouts/feature.html
+---
+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 header=2%}
+    <div id="container" class="mainContainer">
+      <div class="tabs">
+        <div class="wrap">
+		  {% for tab in site.data.tabs %}
+			<a class="tabLink {% if page.active==forloop.index %}active{% endif %}" href="{{ tab.link }}">{{ tab.name }}</a> <em></em> 
+		  {% endfor %} 
+		{% if page.active == 1 %}
+          <div class="tabOptions">
+            <div class="pluginSearch">
+			  <a class="btn" target="_blank" href="frama-c-plugin-development-guide.pdf"><span>Write Your Own Plugin</span></a>
+            </div>
+          </div>
+		{% endif %}
+        </div>
+      </div>
+      <div class="pageKernel pages">
+        <div class="wrap">
+		{{ content }}
+        </div>
+      </div>
+	  {% include footer.html %}
+      <div class="clear"></div>
+    </div>
+  </div>
+</body>
--- a/assets/css/home.css
+++ b/assets/css/home.css
@@ -1165,11 +1165,11 @@ a.goDown .icon {
  opacity: 1;
  transform: translate(0%, 0%);
 }
-.pageContent.follow .bgTitleBlk {
+.pageContent.timeline .bgTitleBlk {
  background: #ccc;
 }
-.pageContent.follow .bgTitleBlk .lowerType,
+.pageContent.timeline .bgTitleBlk .lowerType,
-.pageContent.follow .bgTitleBlk .upperType {
+.pageContent.timeline .bgTitleBlk .upperType {
  color: #d9d9d9;
 }
 .pageContent.lightTxt .bgTitleBlk .lowerType,
@@ -1469,12 +1469,8 @@ a.goDown .icon {
 .calendarScreen {
  /*background: #f6f6f6;*/
  overflow: hidden;
-}
+  height: auto;
-@media (max-width:  767px) {
+  padding-bottom: 120px;
-  .calendarScreen {
-    height: auto;
-    padding-bottom: 120px;
-  }
 }
 .calendarScreen .sectionContent {
  padding: 28px 0 20px;
@@ -1482,67 +1478,28 @@ a.goDown .icon {
 .calendarScreen h2 {
  color: #484848;
  text-transform: none;
+  font-size: 33px;
 }
-@media (min-width:  768px) {
+.eventDetailsBlock {
-  .calendarScreen h2 {
+  margin-top: 200px;
-    font-size: 26px;
-    margin: 20px 0 12vh;
-  }
-}
-@media (min-width: 1024px) {
-  .calendarScreen h2 {
-    font-size: 27px;
-    margin: 3vh 0 11vh;
-  }
-}
-@media (min-width: 1600px) {
-  .calendarScreen h2 {
-    font-size: 29px;
-  }
-}
-@media (min-width: 1890px) {
-  .calendarScreen h2 {
-    font-size: 33px;
-  }
 }
 .eventDetailsBlock .swiper-slide {
  width: 100vw;
  padding-left: 20px;
  padding-right: 20px;
 }
-.eventDetailsBlock figure {
-  width: 100%;
-  box-shadow: 0 20px 20px rgba(0, 0, 0, 0.2);
-  padding-bottom: 57.6%;
-  height: 0;
-  position: relative;
-  margin-bottom: 20px;
-}
-.eventDetailsBlock figure img,
-.eventDetailsBlock figure video,
-.eventDetailsBlock figure .img {
-  background-color: #fff;
-  display: block;
-  width: 100%;
-  position: absolute;
-  top: 0;
-  bottom: 0;
-  left: 0;
-  margin: auto;
-  height: 100%;
-  object-fit: cover;
-}
 .eventDetailsBlock .contentBlk {
-  display: flex;
+  display: inline-flex;
  text-align: left;
  font-size: 13px;
 }
 .eventDetailsBlock .contentBlk > div {
-  margin-left: 14px;
+  margin-left: 16px;
 }
 .eventDetailsBlock .contentBlk h3 {
-  font-size: 17px;
+  font-size: 18px;
  margin: 0 0 8px;
+  margin-bottom: 20px;
 }
 .eventDetailsBlock .contentBlk p {
  font-weight: 600;
@@ -1553,7 +1510,7 @@ a.goDown .icon {
 }
 .eventDetailsBlock time {
  color: #e74643;
-  font-size: 47px;
+  font-size: 32px;
  line-height: 1.1;
 }
 .eventDetailsBlock time b,
@@ -1565,13 +1522,13 @@ a.goDown .icon {
  line-height: 40px;
 }
 .eventDetailsBlock time b + b {
-  font-size: 31px;
+  font-size: 18px;
  margin-top: -1px;
 }
 .eventDetailsBlock time small {
  font-size: 16px;
 }
-@media (min-width:  768px) {
+@media (min-width:  800px) {
  .eventDetailsBlock time {
    font-size: 42px;
    display: inline-flex;
@@ -1584,10 +1541,10 @@ a.goDown .icon {
    margin-top: 0;
  }
  .eventDetailsBlock time small {
-    font-size: 13px;
+    font-size: 18px;
  }
 }
-@media (min-width: 1600px) {
+@media (min-width: 1200px) {
  .eventDetailsBlock time {
    font-size: 50px;
  }
@@ -1595,110 +1552,71 @@ a.goDown .icon {
    font-size: 35px;
  }
  .eventDetailsBlock time small {
-    font-size: 15px;
+    font-size: 21px;
    margin-top: 2px;
  }
 }
-@media (min-width:  768px) {
+@media (min-width: 800px) {
-  .eventDetailsBlock .eventDetail {
-    width: 640px;
-    margin: 0 auto;
-    padding-bottom: 30px;
-  }
-  .eventDetailsBlock .eventDetail figure {
-    display: inline-block;
-    vertical-align: top;
-    width: 300px;
-    padding-bottom: 170px;
-  }
-  .eventDetailsBlock .eventDetail .contentBlk {
-    display: inline-flex;
-    width: 330px;
-    vertical-align: middle;
-    padding: 10px 0 0 15px;
-  }
-}
-@media (min-width: 1024px) {
  .eventDetailsBlock .eventDetail {
-    width: 960px;
+    width: auto;
    padding-bottom: 40px;
  }
-  .eventDetailsBlock .eventDetail figure {
-    width: 400px;
-    padding-bottom: 220px;
-  }
  .eventDetailsBlock .eventDetail .contentBlk {
-    width: 400px;
    padding: 12px 0 0 22px;
    font-size: 14px;
  }
-  .eventDetailsBlock .eventDetail .contentBlk h3 {
-    font-size: 18px;
-    margin-bottom: 12px;
-  }
-}
-@media (min-width: 1600px) {
-  .eventDetailsBlock .eventDetail {
-    width: 1080px;
-  }
-  .eventDetailsBlock .eventDetail figure {
-    width: 500px;
-    padding-bottom: 280px;
-  }
-  .eventDetailsBlock .eventDetail .contentBlk {
-    width: 500px;
-    font-size: 15px;
-  }
  .eventDetailsBlock .eventDetail .contentBlk > div {
-    margin-left: 23px;
+    margin-left: 48px;
  }
  .eventDetailsBlock .eventDetail .contentBlk h3 {
-    font-size: 19px;
+    font-size: 20px;
-    width: 75%;
+    margin-bottom: 25px;
  }
 }
-@media (min-width: 1890px) {
+@media (min-width: 1200px) {
  .eventDetailsBlock .eventDetail {
-    width: 1260px;
+    width: auto;
+    margin-left: 15%;
+    margin-right: 15%;
    padding-bottom: 50px;
  }
-  .eventDetailsBlock .eventDetail figure {
-    width: 625px;
-    padding-bottom: 340px;
-  }
  .eventDetailsBlock .eventDetail .contentBlk {
-    width: 520px;
    padding: 15px 0 0 27px;
    font-size: 16px;
  }
  .eventDetailsBlock .eventDetail .contentBlk > div {
-    margin-left: 27px;
+    margin-left: 64px;
  }
  .eventDetailsBlock .eventDetail .contentBlk h3 {
-    font-size: 20px;
+    font-size: 24px;
-    margin-bottom: 10px;
+    margin-bottom: 30px;
  }
 }
 .eventScaleBlock {
  position: absolute;
-  bottom: 42px;
+  top: 100px;
  left: 0;
  width: 100%;
  /*height: 60px;*/
  z-index: 2;
 }
+@media (min-width: 1200px) {
-@media (min-width: 1024px) {
+  .eventScaleBlock {
-  .eventScaleBlock .swiper-slide {
+    top: 125px;
-    width: 11%;
-    flex-basis: 11%;
  }
-  .eventScaleBlock .swiper-slide-prev,
+  .eventDetailsBlock {
-  .eventScaleBlock .swiper-slide-next {
+    margin-top: 250px;
-    width: 22.5%;
-    flex-basis: 22.5%;
  }
 }
+.eventScaleBlock .swiper-slide {
+    width: auto;
+    flex-basis: auto;
+}
+.eventScaleBlock .swiper-slide-prev,
+.eventScaleBlock .swiper-slide-next {
+    width: auto;
+    flex-basis: auto;
+}
 .eventScaleBlock nav {
  box-sizing: border-box;
  display: flex;
@@ -1744,7 +1662,7 @@ a.goDown .icon {
 }
 .eventScaleBlock .eventLink span {
  position: absolute;
-  opacity: 0;
+  opacity: 1;
  left: 50%;
  text-align: center;
  width: 140px;
@@ -1755,7 +1673,7 @@ a.goDown .icon {
  font-size: 11px;
  padding-top: 12px;
  margin-left: -70px;
-  transform: translateY(-20px);
+  transform: translateY(-10px);
  transition: all 0.6s;
 }
 @media (min-width:  768px) {
@@ -1797,7 +1715,7 @@ a.goDown .icon {
  box-shadow: 0 3px 0 rgba(0, 0, 0, 0.15);
 }
 .nonTouch .eventScaleBlock .eventLink:hover span {
-  opacity: 1;
+  font-weight: bold;
  transform: translateY(0);
 }
 .nonTouch .eventScaleBlock .eventLink:active time {
@@ -1818,7 +1736,8 @@ a.goDown .icon {
  font-size: 14px;
 }
 .eventScaleBlock .swiper-slide-active .eventLink span {
-  opacity: 1;
+  font-weight: bold;
+  color:  #e74643;
  transform: translateY(0px);
 }
 @media (min-width: 1600px) {
@@ -1831,18 +1750,6 @@ a.goDown .icon {
    font-size: 15px;
  }
 }
-.eventScaleBlock .scaleBg {
-  mask-image: url('../img/timeline-mask.png');
-  mask-position: top left;
-  mask-repeat: no-repeat;
-  mask-size: cover;
-  position: absolute;
-  top: 50%;
-  left: 0;
-  width: 100%;
-  height: 12px;
-  margin-top: -6px;
-}
 .eventScaleBlock .scaleBg > u {
  background-image: url('../img/bg-scale.jpg');
  background-repeat: repeat-x;

--- a/assets/css/plugin.css
+++ b/assets/css/plugin.css
@@ -263,50 +263,6 @@
    padding-right: 10px;
  }
 }
-@media (min-width:  768px) {
-  .pagePlugin .bgTextbig,
-  .pluginDetail .bgTextbig {
-    font-size: 200px;
-  }
-}
-@media (min-width: 1024px) {
-  .pagePlugin .bgTextbig,
-  .pluginDetail .bgTextbig {
-    font-size: 260px;
-  }
-}
-@media (min-width: 1280px) {
-  .pagePlugin .bgTextbig,
-  .pluginDetail .bgTextbig {
-    font-size: 300px;
-  }
-}
-@media (min-width: 1600px) {
-  .pagePlugin .bgTextbig,
-  .pluginDetail .bgTextbig {
-    font-size: 360px;
-  }
-}
-@media (min-width:  768px) {
-  .pageKernel .bgTextbig {
-    font-size: 220px;
-  }
-}
-@media (min-width: 1024px) {
-  .pageKernel .bgTextbig {
-    font-size: 280px;
-  }
-}
-@media (min-width: 1280px) {
-  .pageKernel .bgTextbig {
-    font-size: 320px;
-  }
-}
-@media (min-width: 1600px) {
-  .pageKernel .bgTextbig {
-    font-size: 380px;
-  }
-}
 .aboutKernel {
  margin: 70px 0;
  overflow: hidden;

--- a/assets/img/events/Argon.jpg
+++ b/assets/img/events/Argon.jpg
--- a/assets/img/events/Chlorine.jpg
+++ b/assets/img/events/Chlorine.jpg
--- a/assets/img/events/Phosphorus.png
+++ b/assets/img/events/Phosphorus.png
--- a/assets/img/events/Potassium.jpg
+++ b/assets/img/events/Potassium.jpg
--- a/assets/img/events/Sulfur.jpg
+++ b/assets/img/events/Sulfur.jpg
--- a/assets/img/events/fc-day-2019.png
+++ b/assets/img/events/fc-day-2019.png
--- a/assets/img/events/frama-clang.png
+++ b/assets/img/events/frama-clang.png
--- a/assets/js/main.js
+++ b/assets/js/main.js
@@ -10028,13 +10028,13 @@ function home() {
 		var event_calender_swiper = new Swiper('#event_calender_swiper', {
 			spaceBetween: 0,
 			centeredSlides: true,
-			slidesPerView: 7,
+			slidesPerView: 9,
 			resistanceRatio: 0,
 			slideToClickedSlide: true,
 			breakpoints: {
-				1023: {
+			  1400: { slidesPerView: 7 },
-					slidesPerView: 5
+			  1024: { slidesPerView: 5 },
-				}
+			  600: { slidesPerView: 3 }
 			}
 		});
 		event_detail_swiper.params.control = event_calender_swiper;
@@ -10091,7 +10091,7 @@ function home() {
 		callWayPoint('siteIntro_iv_point', 'SECURE', 'secure');
 		callWayPoint('code_demo_iv_point', 'ERROR!', 'error');
 		callWayPoint('about_iv_point', 'ABOUT', 'about');
-		callWayPoint('events_iv_point', 'FOLLOW', 'follow');
+		callWayPoint('events_iv_point', 'TIMELINE', 'timeline');
 		callWayPoint('download_iv_point', 'DOWNLOAD', 'download bigTxt');
 		$(window).trigger('resize');

--- a/html/acsl.html
+++ b/html/acsl.html
 ---
-layout: default
+layout: feature
 css: plugin
 title: ACSL
+active: 3
 ---
-<body class="page-template page-template-page-kernel page-template-page-kernel-php page page-id-179 nonTouch">
+<h1>ANSI/ISO C Specification Language</h1>
-  <div id="wrapper" class="hfeed">
+<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
-	{% include headers.html %}
+inspired of <a class="extlink" href=
+			   "http://www.eecs.ucf.edu/~leavens/JML/index.shtml">JML</a>. It also
+inherits a lot from the specification language of the source code
+analyzer <a class="extlink" href=
+			"http://caduceus.lri.fr/">Caduceus</a>, a previous development of
+one of the partners in the Frama-C project.</p>
+<p>ACSL can express a wide range of functional properties. The
+paramount notion in ACSL is the function contract.
+While many software engineering experts
+advocate the "function contract mindset" when designing complex
+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>
-    <div id="container" class="mainContainer">
+<p>ACSL allows to write contracts that range from the low-level
-      <div class="tabs">
+(“<i>this function expects a valid pointer to int</i>”) to the
-        <div class="wrap">
+high-level (“<i>this function expects a nonempty linked list of
-          <a class="tabLink" href="/html/kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink" href=
+  ints and returns the greatest of these ints</i>”). It is expressive
-          "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink active" href="/html/acsl.html">ACSL</a>
+enough to write complete specifications for many functions, but it
-        </div>
+can also be used for writing partial specifications. Partial
-      </div>
+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>
-      <div class="pageKernel pages">
+<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
+or more interactive, with WP's built-in interactive prover
+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
+properties inside the source code.</p>
-        <div class="wrap">
+<h2>More information</h2>
-          <h1>ANSI/ISO C Specification Language</h1>
+<ul>
-          <h2>Quick description</h2>
+<li>The ACSL manual has its own
-          <p>The ANSI/ISO C Specification Langage (ACSL) is a behavioral
+  <a href="https://github.com/acsl-language/acsl/">repository</a>,
-            specification language for C programs. The design of ACSL is
+  together with ACSL++ (its companion language for specifying C++
-            inspired of <a class="extlink" href=
+  programs and analyzing them with the
-                           "http://www.eecs.ucf.edu/~leavens/JML/index.shtml">JML</a>. It also
+  <a href="../fc-plugins/frama-clang.html">frama-clang</a>
-            inherits a lot from the specification language of the source code
+  plug-in. Pdf versions of the manual are available on the
-            analyzer <a class="extlink" href=
+  <a href="https://github.com/acsl-language/acsl/releases">
-                        "http://caduceus.lri.fr/">Caduceus</a>, a previous development of
+	release page</a>.
-            one of the partners in the Frama-C project.</p>
+</li>
-          <p>ACSL can express a wide range of functional properties. The
+<li>A comprehensive tutorial on
-            paramount notion in ACSL is the function contract.
+  <a href="../fc-plugins/wp.html">the WP plugin</a> and ACSL
-            While many software engineering experts
+  specifications is available
-            advocate the "function contract mindset" when designing complex
+  <a href="https://allan-blanchard.fr/frama-c-wp-tutorial.html">
-            software, they generally leave the actual expression of the
+	here</a>.
-            contract to run-time assertions, or to comments in the source code.
+</li>
-            ACSL is expressly designed for writing the kind of properties that
+<li>Another tutorial, with specifications inspired notably from C++
-            make up a function contract.
+  containers is available
-            ACSL is a <em>formal</em> language. This means that the
+  <a href="https://github.com/fraunhoferfokus/acsl-by-example">
-            specifications written in ACSL can be automatically manipulated by
+	here</a>.
-            helper programs, in the same way that a programming language is a
+</li>
-            formal language manipulated by a compiler, and by opposition to
+</ul>
-            informally written comments that can only be useful to humans.</p>
-          <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>
-          <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
-            or more interactive, with WP's built-in interactive prover
-            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
-            properties inside the source code.</p>
-          <h2>More information</h2>
-          <ul>
-            <li>The ACSL manual has its own
-              <a href="https://github.com/acsl-language/acsl/">repository</a>,
-              together with ACSL++ (its companion language for specifying C++
-              programs and analyzing them with the
-              <a href="../fc-plugins/frama-clang.html">frama-clang</a>
-              plug-in. Pdf versions of the manual are available on the
-              <a href="https://github.com/acsl-language/acsl/releases">
-                release page</a>.
-            </li>
-            <li>A comprehensive tutorial on
-              <a href="../fc-plugins/wp.html">the WP plugin</a> and ACSL
-              specifications is available
-              <a href="https://allan-blanchard.fr/frama-c-wp-tutorial.html">
-                here</a>.
-            </li>
-            <li>Another tutorial, with specifications inspired notably from C++
-              containers is available
-              <a href="https://github.com/fraunhoferfokus/acsl-by-example">
-                here</a>.
-            </li>
-          </ul>
-        </div>
-      </div>
-      {% include footer.html %}
-      <div class="clear"></div>
-    </div>
-  </div>
-</body>
--- a/html/careers.html
+++ b/html/careers.html
@@ -7,7 +7,7 @@ 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 %}
+	{% include headers.html header=5 %}
    <div id="container" class="mainContainer">
      <div class="pageCareers pages">
No results found