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/_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/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/index.html b/index.html
index c8ff1c8b8425730a967f6cf3c05d83d0562a08f1..8bfb77ac860e5048decbc6ef6eeac1642e969040 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.
+ <br style="display: inline;">
+ <span><a href="html/overview.html">Read More</a></span>
</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">