Merge branch 'frama-c-overview' into 'master'

Frama-C Overview page

See merge request !59

html/installations/nitrogen.html

 ---
-layout: clean_page
+layout: doc_page
 title: Installation instructions for Frama-C Nitrogen release
 ---
 

html/installations/oxygen.html

 ---
-layout: clean_page
+layout: doc_page
 title: Installation instructions for Frama-C Oxygen release
 ---
 

html/installations/phosphorus.html

 ---
-layout: clean_page
+layout: doc_page
 title: Installation instructions for Phosphorus
 ---
 

html/installations/potassium.html

 ---
-layout: clean_page
+layout: doc_page
 title: Installation instructions for Potassium
 ---
 

html/installations/scandium.md

 ---
-layout: clean_page
+layout: doc_page
 title: Installation instructions for Scandium
 ---
 

html/installations/silicon.html

 ---
-layout: clean_page
+layout: doc_page
 title: Installation instructions for Silicon
 ---
 

html/installations/sodium.html

 ---
-layout: clean_page
+layout: doc_page
 title: Installation instructions for Sodium
 ---
 

html/installations/sulfur.html

 ---
-layout: clean_page
+layout: doc_page
 title: Installation instructions for Sulfur
 ---
 

html/kernel-plugin.html

@@ -2,7 +2,7 @@
 layout: feature
 css: plugin
 title: Kernel & Plugins - Frama-C
-active: 1
+active: "kernel-plugin"
 ---
 
 

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

html/overview.md

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

html/publications/2010-ensiie-vslg/ensiie2010-2011-ias-tp.md

 ---
 title: ENSIIE - Analyse Statique de Programmes 2010/2011
-layout: clean_page
+layout: doc_page
 ---
 # Analyse Statique de programmes - TP Frama-C
 

html/publications/2010-ensiie-vslg/ensiie2011-2012-ias-tp.md

 ---
 title: ENSIIE - Analyse Statique de Programmes 2011/2012
-layout: clean_page
+layout: doc_page
 ---
 # Analyse Statique de programmes - TP Frama-C
 

html/publications/2010-ensiie-vslg/ensiie2012-2013-ias-tp.md

 ---
 title: ENSIIE - Analyse Statique de Programmes 2012/2013
-layout: clean_page
+layout: doc_page
 ---
 # Analyse Statique de programmes - TP Frama-C
 

html/publications/2010-ensiie-vslg/ensiie2013-2014-ias-tp.md

 ---
 title: ENSIIE - Analyse Statique de Programmes 2013/2014
-layout: clean_page
+layout: doc_page
 ---
 # Analyse Statique de programmes - TP Frama-C
 

html/publications/2010-ensiie-vslg/ensiie2014-2015-ias-tp.md

 ---
 title: ENSIIE - Analyse Statique de Programmes 2014/2015
-layout: clean_page
+layout: doc_page
 ---
 # Analyse Statique de Programmes -- TP Frama-C
 

html/publications/2010-ensiie-vslg/ensiie2015-2016-ias-tp.md

 ---
 title: ENSIIE - Analyse Statique de Programmes 2015/2016
-layout: clean_page
+layout: doc_page
 ---
 # Analyse Statique de Programmes -- TP Frama-C
 

html/publications/2010-ensiie-vslg/ensiie2016-2017-ias-tp.md

 ---
 title: ENSIIE - Analyse Statique de Programmes 2016/2017
-layout: clean_page
+layout: doc_page
 ---
 # Analyse Statique de Programmes -- TP Frama-C
 

html/publications/2010-ensiie-vslg/ensiie2017-2018-ias-tp.md

 ---
 title: ENSIIE - Analyse Statique de Programmes 2017/2018
-layout: clean_page
+layout: doc_page
 ---
 # Analyse Statique de Programmes – TP Frama-C
 

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