diff --git a/_data/nav.yml b/_data/nav.yml
index 91f28a3cba018ad2fa0b9f22032d06accc4e2ffc..3e25bf22891ef5b96e236a3328cda137a52671c8 100644
--- a/_data/nav.yml
+++ b/_data/nav.yml
@@ -1,6 +1,6 @@
-#- name: Using Frama-C
-# link: /html/using-frama-c.html
-# id : using
+- name: Overview
+ link: /html/overview.html
+ id: overview
- name: Features
link: /html/kernel-plugin.html
id : features
diff --git a/_data/tabs.yml b/_data/tabs.yml
index d5032da222a141fe5c4f5f935f569d262e6ebf08..d53e65e64afac9a8a85ad64d154291e6e3d31f3b 100644
--- a/_data/tabs.yml
+++ b/_data/tabs.yml
@@ -1,8 +1,12 @@
- name: Plugins
link: /html/kernel-plugin.html
+ id : kernel-plugin
- name: Kernel
link: /html/kernel.html
+ id : kernel
- name: GUI
link: /html/gui.html
+ id : gui
- name: ACSL
link: /html/acsl.html
+ id : acsl
diff --git a/_layouts/clean_page.html b/_layouts/clean_page.html
index 1364c0fea3797d01d2aeebb84d1570f56936fd87..e572af13bc38ce7483d34ceec82c7112c9edc80c 100644
--- a/_layouts/clean_page.html
+++ b/_layouts/clean_page.html
@@ -1,23 +1,23 @@
----
-layout: default
-css: plugin
----
-
-<body class="page nonTouch">
- <div id="wrapper" class="hfeed">
- {% include headers.html header="documentation" %}
-
- <div id="container" class="mainContainer">
- <div class="tabs">
- <div class="pageKernel pages">
- <div class="wrap">
- {{ content }}
- </div>
- </div>
-
- {% include footer.html %}
-
- <div class="clear"></div>
- </div>
- </div>
-</body>
+---
+layout: default
+css: plugin
+---
+
+<body class="page nonTouch">
+ <div id="wrapper" class="hfeed">
+ {% include headers.html %}
+
+ <div id="container" class="mainContainer">
+ <div class="tabs">
+ <div class="pageKernel pages">
+ <div class="wrap">
+ {{ content }}
+ </div>
+ </div>
+
+ {% include footer.html %}
+
+ <div class="clear"></div>
+ </div>
+ </div>
+
diff --git a/_layouts/doc_page.html b/_layouts/doc_page.html
new file mode 100644
index 0000000000000000000000000000000000000000..5d95a2c8dfd06b5c0354bc22d35e712645c2e201
--- /dev/null
+++ b/_layouts/doc_page.html
@@ -0,0 +1,23 @@
+---
+layout: default
+css: plugin
+---
+
+<body class="page nonTouch">
+ <div id="wrapper" class="hfeed">
+ {% include headers.html header="documentation" %}
+
+ <div id="container" class="mainContainer">
+ <div class="tabs">
+ <div class="pageKernel pages">
+ <div class="wrap">
+ {{ content }}
+ </div>
+ </div>
+
+ {% include footer.html %}
+
+ <div class="clear"></div>
+ </div>
+ </div>
+
diff --git a/_layouts/feature.html b/_layouts/feature.html
index 33ee8311b095a3f405944bbe557e34f059a9c5c7..e91caefcae0a5746c546482125a5601abf3a839e 100644
--- a/_layouts/feature.html
+++ b/_layouts/feature.html
@@ -15,11 +15,11 @@ title: Kernel & Plugins - Frama-C
<div class="wrap">
{% for tab in site.data.tabs %}
<span>
- <a class="tabLink {% if page.active==forloop.index %}active locked{% endif %}" href="{{ tab.link }}">{{ tab.name }}</a>
+ <a class="tabLink {% if page.active==tab.id %}active locked{% endif %}" href="{{ tab.link }}">{{ tab.name }}</a>
</span>
{% endfor %}
- {% if page.active == 1 %}
+ {% if page.active == "kernel-plugin" %}
<span>
<div class="tabOptions">
<div class="pluginSearch">
diff --git a/_layouts/overview_page.html b/_layouts/overview_page.html
new file mode 100644
index 0000000000000000000000000000000000000000..837378a67442cada6fc2fa2efd0678327dd2006b
--- /dev/null
+++ b/_layouts/overview_page.html
@@ -0,0 +1,32 @@
+---
+layout: default
+css: plugin
+---
+
+<body class="page nonTouch">
+ <div id="wrapper" class="hfeed">
+ {% include headers.html header="overview" %}
+
+ <div id="container" class="mainContainer">
+ <div class="tabs">
+ <div class="pageKernel pages">
+ {% if page.video %}
+ <div class="videoHead wrap">
+ <figure>
+ <iframe width="560" height="315" src="{{ page.video }}" frameborder="0" allowfullscreen=""></iframe>
+ </figure>
+ </div>
+ {% endif %}
+ <div class="wrap">
+ <h1 class="pageTitle">Overview of Frama-C</h1>
+
+ {{ content }}
+ </div>
+ </div>
+
+ {% include footer.html %}
+
+ <div class="clear"></div>
+ </div>
+ </div>
+
diff --git a/assets/css/page.css b/assets/css/page.css
index a4a850c6f91d9d1de8e60f72161f50ed3ce6b192..8d66c0b6b5305a1f6a19389a358cc7299044ab02 100644
--- a/assets/css/page.css
+++ b/assets/css/page.css
@@ -577,9 +577,12 @@
margin-right: 5px;
}
}
+.videoHead {
+ margin-bottom: 40px;
+}
@media (min-width: 768px) {
.videoHead {
- margin: 20px auto 0;
+ margin: 40px auto;
width: 86%;
max-width: 1260px;
}
@@ -592,14 +595,12 @@
}
}
.videoHead figure {
- box-shadow: 0 12px 30px 0 rgba(0, 0, 0, 0.25);
position: relative;
width: 100%;
padding-bottom: 56.7%;
}
@media (min-width: 1024px) {
.videoHead figure {
- box-shadow: 0 54px 70px 0 rgba(0, 0, 0, 0.3);
padding-bottom: 42%;
}
}
diff --git a/html/acsl.html b/html/acsl.html
index bf783aedbbc01c31bfe2f6c89b54e933faa1a4f0..2b42d9439bd509f730b6977124a8faed383a753f 100755
--- a/html/acsl.html
+++ b/html/acsl.html
@@ -1,8 +1,8 @@
---
layout: feature
css: plugin
-title: ACSL
-active: 4
+title: ACSL - Frama-C
+active: acsl
---
<h1>ANSI/ISO C Specification Language</h1>
diff --git a/html/bug_reporting_guidelines.md b/html/bug_reporting_guidelines.md
index 9e172ee0bef708776b77bd59fef6645622addfee..ee66048cc257718a38dc052571e49c18d4b85233 100644
--- a/html/bug_reporting_guidelines.md
+++ b/html/bug_reporting_guidelines.md
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Bug reporting
---
# Report an issue with Frama-C
diff --git a/html/gui.md b/html/gui.md
index 103841e8001cc5ece51059a9d1dc20ab53a26185..44dd29db62bdae278c5eb2b979e84e1bb987a223 100644
--- a/html/gui.md
+++ b/html/gui.md
@@ -2,7 +2,7 @@
layout: feature
css: plugin
title: Graphical User Interface (GUI) - Frama-C
-active: 3
+active: gui
---
If the Frama-C kernel is the heart of the platform,
diff --git a/html/installations/aluminium.html b/html/installations/aluminium.html
index 722e7dfb1a02fb075293428c16b1ffc7b6f958a3..66e53503b34a407881bb19f142a37ad7fa664f55 100644
--- a/html/installations/aluminium.html
+++ b/html/installations/aluminium.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Aluminium
---
diff --git a/html/installations/argon.html b/html/installations/argon.html
index 7f759e91a4b949ebe4afcf9e8685431fbfdb05c2..a7b598463035039892d9093a8501288a64dbd2cc 100644
--- a/html/installations/argon.html
+++ b/html/installations/argon.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for 18.0 Argon
---
diff --git a/html/installations/beryllium-OSX.html b/html/installations/beryllium-OSX.html
index 4652908e53f5f74f0357d83b44aa20352a5b2aa0..f6dbd52b80c1c82fddc1b91231c150191542a154 100644
--- a/html/installations/beryllium-OSX.html
+++ b/html/installations/beryllium-OSX.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Beryllium release
---
diff --git a/html/installations/beryllium-why-2.21.html b/html/installations/beryllium-why-2.21.html
index 74380508027ad69f189f7cea5cbc2ff1ebe20166..444b67bcda9285dae6da856d90b2876fef6183f0 100644
--- a/html/installations/beryllium-why-2.21.html
+++ b/html/installations/beryllium-why-2.21.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Beryllium release
---
diff --git a/html/installations/beryllium-windows-20090902.html b/html/installations/beryllium-windows-20090902.html
index e03717a42b5cc3dc2d3e7c1b854705eab981b931..f3dcf87eb3973f4f59fecb4a056327ea407a9ef5 100644
--- a/html/installations/beryllium-windows-20090902.html
+++ b/html/installations/beryllium-windows-20090902.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Beryllium release
---
diff --git a/html/installations/beryllium-windows.html b/html/installations/beryllium-windows.html
index dec4a42281e75301761d9d5f4c7562c9ec635e28..85cce3a61058c1a0fd7384a219cc8a3f2dda651a 100644
--- a/html/installations/beryllium-windows.html
+++ b/html/installations/beryllium-windows.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Beryllium release
---
diff --git a/html/installations/beryllium.html b/html/installations/beryllium.html
index d8cfa236a51eac6b3bcad56e958bf4f2dcf9db1b..572103c6cd5142e40d7d1ea947caa8fef885d260 100644
--- a/html/installations/beryllium.html
+++ b/html/installations/beryllium.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Beryllium release
---
diff --git a/html/installations/boron-OSX.html b/html/installations/boron-OSX.html
index 5677e55376c897b9de1dc4bf149dd4e0b6c8fe67..f25ea88ba57c0a8afa53b1f28d4013d584c0a483 100644
--- a/html/installations/boron-OSX.html
+++ b/html/installations/boron-OSX.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Boron release
---
diff --git a/html/installations/boron-why-2.24.html b/html/installations/boron-why-2.24.html
index 7c0b82951a2ba35af75743ec8ad57537c41ea48d..b99ddf28bc3a75609e3e62770df2165456523a60 100644
--- a/html/installations/boron-why-2.24.html
+++ b/html/installations/boron-why-2.24.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Boron release
---
diff --git a/html/installations/boron-windows.html b/html/installations/boron-windows.html
index 94f11e463a8ee62a062a1755073e682b52432b4a..13e008cf5dd04d4fb058f432262968996267db5e 100644
--- a/html/installations/boron-windows.html
+++ b/html/installations/boron-windows.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Boron release
---
diff --git a/html/installations/boron.html b/html/installations/boron.html
index fa02dcb27050857e43f62ea8f6d3cc3a6b45f3b2..3faf1427065634c7af13667e6139a758c90a57da 100644
--- a/html/installations/boron.html
+++ b/html/installations/boron.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Boron release
---
diff --git a/html/installations/calcium.html b/html/installations/calcium.html
index c57e8ba8845e56747db4c760b85b15c8200d4488..009ca3f4652a5408c20c2c67a98c87c6e373fe9a 100644
--- a/html/installations/calcium.html
+++ b/html/installations/calcium.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Calcium
---
diff --git a/html/installations/carbon-OSX.html b/html/installations/carbon-OSX.html
index f775c935b427b8838013fa5d7c211a3afa77f86f..6bb50dcb73e97eba76141c7f3b86c2c5cba1130f 100644
--- a/html/installations/carbon-OSX.html
+++ b/html/installations/carbon-OSX.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Carbon release
---
diff --git a/html/installations/carbon-beta.html b/html/installations/carbon-beta.html
index 887e6f604cc9cc22233112ff6571e86e6ba6be98..36fc2de3350904429f57694d24afbf178e4b9902 100644
--- a/html/installations/carbon-beta.html
+++ b/html/installations/carbon-beta.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Carbon beta
---
diff --git a/html/installations/carbon-wp.html b/html/installations/carbon-wp.html
index f442b71a571a4d58c7067ff223bdd7106d903abc..1fb72ed3f5ec85ed40d82d20b1451fde6d85c153 100644
--- a/html/installations/carbon-wp.html
+++ b/html/installations/carbon-wp.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C WP Carbon
---
diff --git a/html/installations/carbon.html b/html/installations/carbon.html
index 6cdb4509e14a3dca5613a2c29952cf089962e533..8f259c7bf383c0112e32e25d1956e147eb0ec690 100644
--- a/html/installations/carbon.html
+++ b/html/installations/carbon.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Carbon release
---
diff --git a/html/installations/chlorine.html b/html/installations/chlorine.html
index dc62be0a302ac9fb443af3aad4bb4704a7ace696..b5ff8df5bab7231efc4af88b2b8750c847239290 100644
--- a/html/installations/chlorine.html
+++ b/html/installations/chlorine.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Chlorine
---
diff --git a/html/installations/fluorine-20130401.html b/html/installations/fluorine-20130401.html
index 53004154bc6eb53c530f80464575ff11c4c1f17a..5287c4bd1b2fe189bad4ff211ca3ceeb04b69a8e 100644
--- a/html/installations/fluorine-20130401.html
+++ b/html/installations/fluorine-20130401.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Fluorine
---
diff --git a/html/installations/fluorine-20130501.html b/html/installations/fluorine-20130501.html
index 11df8789116f63c98b12b06b03b43f98aa9273e6..dae540f6a5374cdb4f6c3d3553cb434b2cb53b6e 100644
--- a/html/installations/fluorine-20130501.html
+++ b/html/installations/fluorine-20130501.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Fluorine 2
---
diff --git a/html/installations/fluorine-20130601.html b/html/installations/fluorine-20130601.html
index 950e1d5c87706ec69808234a403e63a0a9f258ce..08ccf4b1b52a1b97ae93552eb67734240dbf7e80 100644
--- a/html/installations/fluorine-20130601.html
+++ b/html/installations/fluorine-20130601.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Fluorine 3
---
diff --git a/html/installations/helium.html b/html/installations/helium.html
index 305b276e0465686b8d1f6b48a2c0b8e3a1fda665..6ab8b334a4914bd5af1228658565639eab85d723 100644
--- a/html/installations/helium.html
+++ b/html/installations/helium.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Helium release
---
diff --git a/html/installations/hydrogen.html b/html/installations/hydrogen.html
index 82bd9ab50998cbfa9e24241e894d6343c72ccee5..72ee6eb092f87616895409e787b2ff94f21de26b 100644
--- a/html/installations/hydrogen.html
+++ b/html/installations/hydrogen.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Hydrogen release
---
diff --git a/html/installations/lithium-OSX.html b/html/installations/lithium-OSX.html
index 71085235a87015bb7fb06b3b23437f0ab0e62f82..acac7961a324e9387033818a3c8489c72caa0426 100644
--- a/html/installations/lithium-OSX.html
+++ b/html/installations/lithium-OSX.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Lithium release
---
diff --git a/html/installations/lithium-windows.html b/html/installations/lithium-windows.html
index c255bb1fc543612b651992269818312e167bc3ad..bd8e2ab6e9d4c166ba36d416ae6f655d15857209 100644
--- a/html/installations/lithium-windows.html
+++ b/html/installations/lithium-windows.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Lithium release
---
diff --git a/html/installations/lithium.html b/html/installations/lithium.html
index 8a17edcc0189fb66bf846a60d780b429262144c1..577cc339bd5af1b630ff0abd567fe84aca21073e 100644
--- a/html/installations/lithium.html
+++ b/html/installations/lithium.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Lithium release
---
diff --git a/html/installations/magnesium.html b/html/installations/magnesium.html
index a425fbbbe899ab3669f85b399aaebb8a61e3e20b..2b628f5d234d837922f0536e08060374d56cc021 100644
--- a/html/installations/magnesium.html
+++ b/html/installations/magnesium.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Magnesium
---
diff --git a/html/installations/neon.html b/html/installations/neon.html
index 916610d12b14f3dd22e4f6edb6624e499b718320..d6a6d9b864f1c27cda842f7bd7b50564086961ca 100644
--- a/html/installations/neon.html
+++ b/html/installations/neon.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Neon
---
diff --git a/html/installations/nitrogen-OSX-intel.html b/html/installations/nitrogen-OSX-intel.html
index e9c26f0c0270dd71393ad65a8c1b122fddce5875..85e8c07d580aa290b73a3c386a3ba48695a6be83 100644
--- a/html/installations/nitrogen-OSX-intel.html
+++ b/html/installations/nitrogen-OSX-intel.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Nitrogen release
---
diff --git a/html/installations/nitrogen-OSX-ppc.html b/html/installations/nitrogen-OSX-ppc.html
index 48e77945a249224cbf5e2daf2ff46583888dbaa6..1e1f24fc31c82d19a32677b1541b7ffa749257df 100644
--- a/html/installations/nitrogen-OSX-ppc.html
+++ b/html/installations/nitrogen-OSX-ppc.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Nitrogen release
---
diff --git a/html/installations/nitrogen-wp.html b/html/installations/nitrogen-wp.html
index 5a4253ba652e12059f24e2c7f30847f8f50947a0..f57a8bb88ba6fceeac311d9865097d5ebca95e2f 100644
--- a/html/installations/nitrogen-wp.html
+++ b/html/installations/nitrogen-wp.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Nitrogen release
---
diff --git a/html/installations/nitrogen.html b/html/installations/nitrogen.html
index ff9011d663f92e7b0fd6dd69e4fe16d7cc889e22..cf3aea48cfd731caea0c39c70f97a8ab068c52d2 100644
--- a/html/installations/nitrogen.html
+++ b/html/installations/nitrogen.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Nitrogen release
---
diff --git a/html/installations/oxygen.html b/html/installations/oxygen.html
index 2351e371faf60310c52088000dcda00a3f1cb601..813c2c911255a7747f520aff8243c113161ccae7 100644
--- a/html/installations/oxygen.html
+++ b/html/installations/oxygen.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Frama-C Oxygen release
---
diff --git a/html/installations/phosphorus.html b/html/installations/phosphorus.html
index 678bb20af473073807fbacb48796bc3a4663ef39..fd37292e69dff6472678d3d77c2712b4b57c8271 100644
--- a/html/installations/phosphorus.html
+++ b/html/installations/phosphorus.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Phosphorus
---
diff --git a/html/installations/potassium.html b/html/installations/potassium.html
index 0293242111f4a715bff6f9071121204322e8f55f..049e378fd7124e3080eec3f517dfc288b9f3b61b 100644
--- a/html/installations/potassium.html
+++ b/html/installations/potassium.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Potassium
---
diff --git a/html/installations/scandium.md b/html/installations/scandium.md
index 00a33b62ed24059902cb7b3c84ea895c217d69cf..12c9f62fba85ac6029d8d9a3531a42ffd2d3f87d 100644
--- a/html/installations/scandium.md
+++ b/html/installations/scandium.md
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Scandium
---
diff --git a/html/installations/silicon.html b/html/installations/silicon.html
index 565451f3d44ffdbf87b22b5da0fea21b03132f57..4e80ae2156e1736d4b61a0653a6c95dd48a41d1a 100644
--- a/html/installations/silicon.html
+++ b/html/installations/silicon.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Silicon
---
diff --git a/html/installations/sodium.html b/html/installations/sodium.html
index 807456360160a55d0fabaac0dd4ccf374315c313..2668252600d1425338e3ac7b323c5600ad24a764 100644
--- a/html/installations/sodium.html
+++ b/html/installations/sodium.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Sodium
---
diff --git a/html/installations/sulfur.html b/html/installations/sulfur.html
index d355793a29e24ea9a237c6d46d45b7433663a146..af46405c2d46c88239b86efb834aa4cb89e973c4 100644
--- a/html/installations/sulfur.html
+++ b/html/installations/sulfur.html
@@ -1,5 +1,5 @@
---
-layout: clean_page
+layout: doc_page
title: Installation instructions for Sulfur
---
diff --git a/html/kernel-plugin.html b/html/kernel-plugin.html
index f7d1cffecbe8b02ffd7748fd574073358c2af945..c592d797e4625e2eb2eb77cd61339879ec6929fa 100755
--- a/html/kernel-plugin.html
+++ b/html/kernel-plugin.html
@@ -2,7 +2,7 @@
layout: feature
css: plugin
title: Kernel & Plugins - Frama-C
-active: 1
+active: "kernel-plugin"
---
diff --git a/html/kernel.html b/html/kernel.html
index 757b0770caa3079a486d1db91467d176a5598b0a..8ab71e3bd39ffa998a3b51708dcc97613b1772c8 100755
--- a/html/kernel.html
+++ b/html/kernel.html
@@ -2,7 +2,7 @@
layout: feature
css: plugin
title: Kernel & Plugins - Frama-C
-active: 2
+active: kernel
---
<p>The Frama-C platform allows checking security, verifying requirements and
diff --git a/html/overview.md b/html/overview.md
new file mode 100644
index 0000000000000000000000000000000000000000..68bb2056d37909cfc7ab0b921dd52074baa3081d
--- /dev/null
+++ b/html/overview.md
@@ -0,0 +1,59 @@
+---
+layout: overview_page
+css: plugin
+title: Overview - Frama-C
+video: "https://www.youtube.com/embed/WBXPDfz2u1c"
+---
+
+# What is Frama-C?
+
+Frama-C is a suite of tools dedicated to the analysis of the source code of
+software written in C or C++.
+
+Frama-C gathers several static and dynamic analysis techniques in a single
+collaborative framework. The collaborative approach of Frama-C allows static
+analyzers to build upon the results already computed by other analyzers in the
+framework.
+
+# Static Analysis?
+
+Static analysis of source code is the science of computing synthetic
+information about the source code without executing it.
+
+To most programmers, static analysis means measuring the source code with
+respect to various metrics (examples are the number of comments per line of
+code and the depth of nested control structures). This kind of syntactic
+analysis can be implemented in Frama-C but it is not the focus of the
+project.
+
+Others may be familiar with heuristic bug-finding tools. These tools take
+more of an in-depth look at the source code and try to pinpoint dangerous
+constructions and likely bugs (locations in the code where an error might
+happen at run-time). These heuristic tools do not find all such bugs, and
+sometimes they alert the user for constructions which are in fact not bugs.
+
+Frama-C is closer to these heuristic tools than it is to software metrics
+tools, but it has two important differences with them: it aims at being
+correct, that is, never to remain silent for a location in the source code
+where an error can happen at run-time. And it allows its user to manipulate
+functional specifications, and to prove that the source code satisfies these
+specifications.
+
+Frama-C is not the only correct static analyzer out there, but analyzers of the
+"correct" family are less widely known and used. Software metrics tools do not
+guarantee anything about the behavior of the program, only about the way it is
+written. Heuristic bug-finding tools can be very useful, but because they do
+not find all bugs, they can not be used to prove the absence of bugs in a
+program. Frama-C on the other hand can guarantee that there are no bugs in a
+program ("no bugs" meaning either no possibility of a run-time error, or even
+no deviation from the functional specification the program is supposed to
+adhere to). This of course requires more work from the user than heuristic
+bug-finding tools usually do, but some of the analyses provided by Frama-C
+require comparatively little intervention from the user, and the collaborative
+approach proposed in Frama-C allows the user to get some impressive results.
+
+You may now want to go on to
+[the description of Frama-C's features](/html/kernel-plugin.html), to
+[a page with more details about its modular, extensible architecture](/html/kernel.html),
+or you may want to
+[see Frama-C in action on an example](/index.html#frama-c-overview).
\ No newline at end of file
diff --git a/html/publications/2010-ensiie-vslg/ensiie2010-2011-ias-tp.md b/html/publications/2010-ensiie-vslg/ensiie2010-2011-ias-tp.md
index 39ffc27967e88d2f717c4d301e8881369e675350..4573ff3a2098ad308db20cd156cfd2e4f53acad2 100644
--- a/html/publications/2010-ensiie-vslg/ensiie2010-2011-ias-tp.md
+++ b/html/publications/2010-ensiie-vslg/ensiie2010-2011-ias-tp.md
@@ -1,6 +1,6 @@
---
title: ENSIIE - Analyse Statique de Programmes 2010/2011
-layout: clean_page
+layout: doc_page
---
# Analyse Statique de programmes - TP Frama-C
diff --git a/html/publications/2010-ensiie-vslg/ensiie2011-2012-ias-tp.md b/html/publications/2010-ensiie-vslg/ensiie2011-2012-ias-tp.md
index be881648f631a6a996154fb2f31e5b6b00693d36..7b2e6e44fd21e58b67d966361acc24933df1fee6 100644
--- a/html/publications/2010-ensiie-vslg/ensiie2011-2012-ias-tp.md
+++ b/html/publications/2010-ensiie-vslg/ensiie2011-2012-ias-tp.md
@@ -1,6 +1,6 @@
---
title: ENSIIE - Analyse Statique de Programmes 2011/2012
-layout: clean_page
+layout: doc_page
---
# Analyse Statique de programmes - TP Frama-C
diff --git a/html/publications/2010-ensiie-vslg/ensiie2012-2013-ias-tp.md b/html/publications/2010-ensiie-vslg/ensiie2012-2013-ias-tp.md
index 104b6835a6f391ef383d7b577f434da4dce97777..1ba77e25fe9f6cfefaf8dd74f61d127be742243b 100644
--- a/html/publications/2010-ensiie-vslg/ensiie2012-2013-ias-tp.md
+++ b/html/publications/2010-ensiie-vslg/ensiie2012-2013-ias-tp.md
@@ -1,6 +1,6 @@
---
title: ENSIIE - Analyse Statique de Programmes 2012/2013
-layout: clean_page
+layout: doc_page
---
# Analyse Statique de programmes - TP Frama-C
diff --git a/html/publications/2010-ensiie-vslg/ensiie2013-2014-ias-tp.md b/html/publications/2010-ensiie-vslg/ensiie2013-2014-ias-tp.md
index 877c87098b58146157e290891056c4bb2411538b..1d83c47363c719478fab0b6457ab6e00cc0f5dff 100644
--- a/html/publications/2010-ensiie-vslg/ensiie2013-2014-ias-tp.md
+++ b/html/publications/2010-ensiie-vslg/ensiie2013-2014-ias-tp.md
@@ -1,6 +1,6 @@
---
title: ENSIIE - Analyse Statique de Programmes 2013/2014
-layout: clean_page
+layout: doc_page
---
# Analyse Statique de programmes - TP Frama-C
diff --git a/html/publications/2010-ensiie-vslg/ensiie2014-2015-ias-tp.md b/html/publications/2010-ensiie-vslg/ensiie2014-2015-ias-tp.md
index 645e97fe5d290a57016de6cd9626d2ea877632b4..a243bea7a585248ac9e99dce6d81c2aebb0de343 100644
--- a/html/publications/2010-ensiie-vslg/ensiie2014-2015-ias-tp.md
+++ b/html/publications/2010-ensiie-vslg/ensiie2014-2015-ias-tp.md
@@ -1,6 +1,6 @@
---
title: ENSIIE - Analyse Statique de Programmes 2014/2015
-layout: clean_page
+layout: doc_page
---
# Analyse Statique de Programmes -- TP Frama-C
diff --git a/html/publications/2010-ensiie-vslg/ensiie2015-2016-ias-tp.md b/html/publications/2010-ensiie-vslg/ensiie2015-2016-ias-tp.md
index 72ec0bb570805e9aa013fa23851bc311bea0e43b..12f25104e1c83397a8867e0461240de4deb9f86a 100644
--- a/html/publications/2010-ensiie-vslg/ensiie2015-2016-ias-tp.md
+++ b/html/publications/2010-ensiie-vslg/ensiie2015-2016-ias-tp.md
@@ -1,6 +1,6 @@
---
title: ENSIIE - Analyse Statique de Programmes 2015/2016
-layout: clean_page
+layout: doc_page
---
# Analyse Statique de Programmes -- TP Frama-C
diff --git a/html/publications/2010-ensiie-vslg/ensiie2016-2017-ias-tp.md b/html/publications/2010-ensiie-vslg/ensiie2016-2017-ias-tp.md
index a7de7390fecb3e957dd50c963834ee41b83ea4e7..43e549ae40309afc80f8c2f7a9d952545a8120a5 100644
--- a/html/publications/2010-ensiie-vslg/ensiie2016-2017-ias-tp.md
+++ b/html/publications/2010-ensiie-vslg/ensiie2016-2017-ias-tp.md
@@ -1,6 +1,6 @@
---
title: ENSIIE - Analyse Statique de Programmes 2016/2017
-layout: clean_page
+layout: doc_page
---
# Analyse Statique de Programmes -- TP Frama-C
diff --git a/html/publications/2010-ensiie-vslg/ensiie2017-2018-ias-tp.md b/html/publications/2010-ensiie-vslg/ensiie2017-2018-ias-tp.md
index 3239dab4ed56cb3530276168d99fc5721f7a5630..0ea803ee848fc8699d9cd607a507bf567c62e8ed 100644
--- a/html/publications/2010-ensiie-vslg/ensiie2017-2018-ias-tp.md
+++ b/html/publications/2010-ensiie-vslg/ensiie2017-2018-ias-tp.md
@@ -1,6 +1,6 @@
---
title: ENSIIE - Analyse Statique de Programmes 2017/2018
-layout: clean_page
+layout: doc_page
---
# Analyse Statique de Programmes – TP Frama-C
diff --git a/index.html b/index.html
index c8ff1c8b8425730a967f6cf3c05d83d0562a08f1..aa98c7d686956c719630748d7e2b016822505334 100755
--- a/index.html
+++ b/index.html
@@ -20,6 +20,8 @@ title: Frama-C
source-code analysis of C and C++ software. The Frama-C analyzers assist you
in various source-code-related activities, from the navigation through
unfamiliar projects up to the certification of critical software.
+ <h3><a href="html/overview.html">Read More</a></h3>
+ <br/>
</p>
<a class="btn cta-download" href="/html/get-frama-c.html"><span>Download <b>Frama-C</b><span><i class=
"icon icon-curly-left"></i><i class="icon icon-download-arrow"></i><i class=
@@ -30,7 +32,7 @@ title: Frama-C
<section class="section fullScreen codeDemoScreen textCenter">
<div class="sectionContent">
- <h3 tabindex="0">Overview of a Frama-C analysis for<br>
+ <h3 tabindex="0" id="frama-c-overview" class="anchor">Overview of a Frama-C analysis for<br>
a simple C program</h3>
<div class="slideHeader">