diff --git a/_config.yml b/_config.yml
index ca3dadf2791f1e53a9b1bd566184f81bc90a8399..19953b4750d256911700baa2cf1c6286e201128d 100644
--- a/_config.yml
+++ b/_config.yml
@@ -43,6 +43,7 @@ collections:
output: true
events:
output: false
+ sort_by: date
fc-versions:
output: true
sort_by: number
diff --git a/_data/authors.yml b/_data/authors.yml
index d356d5b35eae52fa306d191756be03ae35f7ec57..d33799d08cec0112a4f9ffaef90faab435d97dbd 100644
--- a/_data/authors.yml
+++ b/_data/authors.yml
@@ -1,16 +1,41 @@
+- Michele Alberti
+- Thibaud Antignac
+- Gergö Barany
+- Patrick Baudin
+- Allan Blanchard
+- Lionel Blatter
- François Bobot
-- Loïc Correnson
- Richard Bonichon
+- Quentin Bouillaguet
+- David Bühler
+- Zakaria Chihani
+- Loïc Correnson
+- Julien Crétin
- Pascal Cuoq
- Zaynah Dargaye
- Jean-Christophe Filliâtre
- Philippe Herrmann
+- Maxime Jacquemin
- Florent Kirchner
+- Tristan Le Gall
+- Jean-Christophe Léchenet
- Matthieu Lemerre
+- Dara Ly
+- David Maison
- Claude Marché
+- André Maroneze
+- Thibault Martin
+- Fonenantsoa Maurica
+- Melody Méaulle
- Benjamin Monate
- Yannick Moy
- Anne Pacalet
+- Valentin Perrelle
+- Guillaume Petiot
- Virgile Prevosto
+- Armand Puccetti
+- Virgile Robles
+- Muriel Roger
- Julien Signoles
-- Boris Yakobowski
+- Kostyantyn Vorobyov
+- Boris Yakobowski
diff --git a/_events/clang-0.7.md b/_events/clang-0.7.md
new file mode 100644
index 0000000000000000000000000000000000000000..ebc0c652775094cb261cab11be0d3453f0a83025
--- /dev/null
+++ b/_events/clang-0.7.md
@@ -0,0 +1,8 @@
+---
+layout: default
+date: 13-09-2019
+title: Release of Frama-C Clang 0.0.7
+image: /assets/img/events/frama-clang.png
+---
+
+Frama-C Clang 0.0.7 is out. Download it [here](/fc-plugins/frama-clang.html).
\ No newline at end of file
diff --git a/_events/event1.md b/_events/event1.md
deleted file mode 100644
index a199af84bd47c5ed7f7e5e17a59b908664cb458f..0000000000000000000000000000000000000000
--- a/_events/event1.md
+++ /dev/null
@@ -1,5 +0,0 @@
----
-layout: default
-date: 10-08-2019
-title: A new day in Frama-C
----
diff --git a/_events/event2.md b/_events/event2.md
deleted file mode 100644
index a199af84bd47c5ed7f7e5e17a59b908664cb458f..0000000000000000000000000000000000000000
--- a/_events/event2.md
+++ /dev/null
@@ -1,5 +0,0 @@
----
-layout: default
-date: 10-08-2019
-title: A new day in Frama-C
----
diff --git a/_events/fc-day-2019.md b/_events/fc-day-2019.md
new file mode 100644
index 0000000000000000000000000000000000000000..565fb6da5955308fc5e86ecd23c485106c379706
--- /dev/null
+++ b/_events/fc-day-2019.md
@@ -0,0 +1,9 @@
+---
+layout: default
+date: 18-05-2019
+title: Frama-C & SPARK Day 2019
+image: /assets/img/events/fc-day-2019.png
+---
+
+Frama-C & SPARK Day 2019 will take place on June 3, 2019 in Paris.
+Registration and program [here](http://frama-c.com/FCSD19.html).
\ No newline at end of file
diff --git a/_events/framac-17.0.md b/_events/framac-17.0.md
new file mode 100644
index 0000000000000000000000000000000000000000..e5f7a32be6242e6dbc744dd891c925ab71019059
--- /dev/null
+++ b/_events/framac-17.0.md
@@ -0,0 +1,8 @@
+---
+layout: default
+date: 31-05-2018
+title: Release of Frama-C 17.0 (Chlorine)
+image: /assets/img/events/Chlorine.jpg
+---
+
+Frama-C 17.0 (Chlorine) is out. Download it [here](/fc-versions/chlorine.html).
\ No newline at end of file
diff --git a/_events/framac-18.0.md b/_events/framac-18.0.md
new file mode 100644
index 0000000000000000000000000000000000000000..88c18410a7b93a82c52ef9832e602a6cd92ae3bb
--- /dev/null
+++ b/_events/framac-18.0.md
@@ -0,0 +1,8 @@
+---
+layout: default
+date: 29-10-2018
+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
diff --git a/_events/framac-19.0.md b/_events/framac-19.0.md
new file mode 100644
index 0000000000000000000000000000000000000000..19a0656a28f3110e2201f8006e9cd5d501136647
--- /dev/null
+++ b/_events/framac-19.0.md
@@ -0,0 +1,8 @@
+---
+layout: default
+date: 21-06-2019
+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
diff --git a/_events/framac-19.1.md b/_events/framac-19.1.md
new file mode 100644
index 0000000000000000000000000000000000000000..bcc2f96f6986435d61b6a341d170517ab7b47d4f
--- /dev/null
+++ b/_events/framac-19.1.md
@@ -0,0 +1,8 @@
+---
+layout: default
+date: 17-09-2019
+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
diff --git a/_fc-plugins/eva.html b/_fc-plugins/eva.html
index 89e64084ad866baf8ea61045b965822858e45520..fb224c3e704e02691a981939ddec953758c1966b 100755
--- a/_fc-plugins/eva.html
+++ b/_fc-plugins/eva.html
@@ -1,6 +1,6 @@
---
layout: plugin
-title: Evolved Value Analysis (EVA)
+title: Eva, an Evolved Value Analysis
description: Automatically computes variation domains for the variables of the program.
key: main
swipper: yes
@@ -18,9 +18,10 @@ swipper: yes
although the user may guide the analysis in places. It handles a wide spectrum of C constructs. This plug-in uses
abstract interpretation techniques.</p>
- <p>The results of <b>EVA</b> can be exploited directly in two ways.</p>
<img src="/assets/img/plugins/eva-img.png">
+ <p>The results of <b>Eva</b> can be exploited directly in two ways.</p>
+
<ul>
<li>They can be used to infer the absence of run-time errors. The results are displayed in reverse, that is,
alarms are emitted for all the operations that could lead to a run-time error. If an alarm is not emitted for an
@@ -29,8 +30,6 @@ swipper: yes
<li>The Frama-C graphical user interface displays the inferred sets for possible values of a variable in each
point of the analyzed program.</li>
</ul>
-
- <p>Maturity: industrialized.</p>
</dd>
<dt class="subTitle">Quick Start</dt>
@@ -39,15 +38,15 @@ swipper: yes
<p>The plug-in can be used both with the graphical user interface and in batch mode. In batch mode, the command
line may look like:</p>
<pre>
-frama-c -val file1.c file2.c
+frama-c -eva file1.c file2.c
</pre>
<p>A list of alarms (corresponding to possible run-time errors as computed by the analysis) is produced on the
standard output.</p>
- <p>The results of <b>EVA</b> are used by many other plug-ins. In this cases, the analysis is initiated
+ <p>The results of <b>Eva</b> are used by many other plug-ins. In this cases, the analysis is initiated
automatically by the exploiting plug-in, but it is still possible to configure it for the case at hand (<i>e.g.</i>
- through the same command-line options that would be used in conjunction with <tt>-val</tt>).</p>
+ through the same command-line options that would be used in conjunction with <tt>-eva</tt>).</p>
</dd>
<dt class="subTitle">First Example</dt>
@@ -67,12 +66,12 @@ int abs(int x) {
Eva also displays the possible values of the variables at the end of the function. Here, we can see that the result
is always positive.</p>
<pre>
-$ frama-c -val test.c -main abs
+$ frama-c -eva test.c -main abs
[…]
-mytests/test.c:2:[value] warning: signed overflow. assert -x ≤ 2147483647;
-[value] done for function abs
-[value] ====== VALUES COMPUTED ======
-[value:final-states] Values at end of function abs:
+mytests/test.c:2:[eva] warning: signed overflow. assert -x ≤ 2147483647;
+[eva] done for function abs
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function abs:
__retres ∈ [0..2147483647]
</pre>
@@ -83,6 +82,8 @@ mytests/test.c:2:[value] warning: signed overflow. assert -x ≤ 2147483647;
<dt class="subTitle">Technical Notes</dt>
<dd>
+ <p>Maturity: industrialized.</p>
+
<p>Recursive calls are currently not supported.</p>
<p>Only sequential code can be analyzed at this time.</p>
@@ -92,10 +93,10 @@ mytests/test.c:2:[value] warning: signed overflow. assert -x ≤ 2147483647;
<dd>
<p>The options to configure the analysis as well as the syntax of the results are described in the <a class="plain"
- href="/download/frama-c-value-analysis.pdf">EVA user manual</a>.</p>
+ href="/download/frama-c-value-analysis.pdf">Eva user manual</a>.</p>
</dd>
<dt class="subTitle"></dt>
<dd></dd>
-</dl>
\ No newline at end of file
+</dl>
diff --git a/_fc-plugins/mthread.html b/_fc-plugins/mthread.html
index 33d2ce9313bb7cf452ddf2d4578e13a9d686500a..04b7189852e8a31b1c9805d4275bd5f0e0ba985d 100755
--- a/_fc-plugins/mthread.html
+++ b/_fc-plugins/mthread.html
@@ -10,8 +10,8 @@ key: concurrent
<dt class="subTitle">Overview</dt>
<dd>
- <p>The <b>Mthread</b> plug-in automatically analyzes concurrent C programs, using the techniques used by the Value
- analysis. At the end of its execution, the concurrent behavior of each thread is over-approximated. Thus, the
+ <p>The <b>Mthread</b> plug-in automatically analyzes concurrent C programs, using the techniques used by Eva.
+ At the end of its execution, the concurrent behavior of each thread is over-approximated. Thus, the
information delivered by the plug-in take into account all the <i>possible concurrent behaviors</i> of the
program.</p>
@@ -36,7 +36,7 @@ key: concurrent
"http://localhost:8000/documentation/mthread/download/frama-c-mthread-graph.svg">this graph</a>.
</li>
- <li>For each program point of each thread, an over approximation of the possible values</li>
+ <li>For each program point of each thread, an over-approximation of the possible values</li>
</ul>
</dd>
@@ -119,6 +119,6 @@ key: concurrent
<dd>
<p>For any questions, remarks or suggestions, please contact <a class="email" href=
- "mailto:boris.yakobowski@cea.fr?subject=[Mthread]">Boris Yakobowski</a>.</p>
+ "mailto:tristan.le-gall@cea.fr?subject=[Mthread]">Tristan Le Gall</a>.</p>
</dd>
-</dl>
\ No newline at end of file
+</dl>
diff --git a/_fc-plugins/studia.html b/_fc-plugins/studia.html
index 903c7f65e78d10cb22b944458e2030bd91ea4772..86563e4186f1d529eb6b22696a4d00d1915062ea 100755
--- a/_fc-plugins/studia.html
+++ b/_fc-plugins/studia.html
@@ -18,7 +18,7 @@ key: browsing
<dt class="subTitle">Quick Start</dt>
<dd>
- <p><code>$ frama-c-gui -val studia.c</code></p>
+ <p><code>$ frama-c-gui -eva studia.c</code></p>
<p>Right-click on an expression in the code and choose the <strong>Studia</strong> context menu to access its
features.</p><img class="size-full wp-image-640" src="/assets/img/plugins/studia-img.png" alt="" width="630" height="189"
@@ -64,4 +64,4 @@ key: browsing
<dd>
<p>Automatically enabled after running EVA and opening the GUI.</p>
</dd>
-</dl>
\ No newline at end of file
+</dl>
diff --git a/assets/css/contact.css b/assets/css/contact.css
index a1a21dae4d24847c3c49ec54254d15f866a47a59..7fd33cbc1b1114c05a6679919ff72f7ecd6a3c88 100644
--- a/assets/css/contact.css
+++ b/assets/css/contact.css
@@ -101,6 +101,7 @@
height: 40px;
border: 0;
border-bottom: 2px solid #b3b3b3;
+ background: #fff0;
transition: border 0.4s, background 0.4s;
}
@media (min-width: 768px) {
diff --git a/assets/img/author/inria.jpg b/assets/img/author/inria.jpg
deleted file mode 100644
index e000305f0f7e3d00a4312df654a2813b5d2a5885..0000000000000000000000000000000000000000
Binary files a/assets/img/author/inria.jpg and /dev/null differ
diff --git a/assets/img/author/inria.png b/assets/img/author/inria.png
new file mode 100644
index 0000000000000000000000000000000000000000..4663638d7189764401570b2054cd1d30dfa08f74
Binary files /dev/null and b/assets/img/author/inria.png differ
diff --git a/assets/img/events/Argon.jpg b/assets/img/events/Argon.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..1964cc381fa38ef52ed41a1235fc97eb18f9def6
Binary files /dev/null and b/assets/img/events/Argon.jpg differ
diff --git a/assets/img/events/Chlorine.jpg b/assets/img/events/Chlorine.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..dff5786e55bbc3ff08d87fb97b83071f18384551
Binary files /dev/null and b/assets/img/events/Chlorine.jpg differ
diff --git a/assets/img/events/Phosphorus.png b/assets/img/events/Phosphorus.png
new file mode 100644
index 0000000000000000000000000000000000000000..bfe2e10953dbd15e0e71f6f22bd72fceb12ca4be
Binary files /dev/null and b/assets/img/events/Phosphorus.png differ
diff --git a/assets/img/events/Potassium.jpg b/assets/img/events/Potassium.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..67f104c68437ede4fc31ef2b49f38f2e2013d114
Binary files /dev/null and b/assets/img/events/Potassium.jpg differ
diff --git a/assets/img/events/Sulfur.jpg b/assets/img/events/Sulfur.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..0541642d11357d3be1ed24e215fae47884589f9e
Binary files /dev/null and b/assets/img/events/Sulfur.jpg differ
diff --git a/assets/img/events/fc-day-2019.png b/assets/img/events/fc-day-2019.png
new file mode 100644
index 0000000000000000000000000000000000000000..dcac53d631301e03c4336bb85dde0a3066cdc631
Binary files /dev/null and b/assets/img/events/fc-day-2019.png differ
diff --git a/assets/img/events/frama-clang.png b/assets/img/events/frama-clang.png
new file mode 100644
index 0000000000000000000000000000000000000000..03c6cec5a24f31e7c44a6295c0efd7dff53dde71
Binary files /dev/null and b/assets/img/events/frama-clang.png differ
diff --git a/dokuwiki/external_plugins.md b/dokuwiki/external_plugins.md
index 4ee34c090270a2ce1a536059ed847f9d5d49a16d..28429e774a9b27bc09e7839dcc48508529ad0133 100644
--- a/dokuwiki/external_plugins.md
+++ b/dokuwiki/external_plugins.md
@@ -1,6 +1,6 @@
----
-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
diff --git a/dokuwiki/faq.md b/dokuwiki/faq.md
deleted file mode 100644
index 02ed335f18ed613d058925c2b6c5da6ac200a1e0..0000000000000000000000000000000000000000
--- a/dokuwiki/faq.md
+++ /dev/null
@@ -1,178 +0,0 @@
----
-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).
diff --git a/dokuwiki/frequently_asked_questions.md b/dokuwiki/frequently_asked_questions.md
deleted file mode 100644
index e4a417c0cd91b8558e01635b12172324c7d348e4..0000000000000000000000000000000000000000
--- a/dokuwiki/frequently_asked_questions.md
+++ /dev/null
@@ -1,1486 +0,0 @@
----
-layout: clean_page
----
-# Some Frequently Asked Questions
-
-The following questions have been collected on the Frama-C mailing list
-([lists.gforge.inria.fr/pipermail/frama-c-discuss](http://lists.gforge.inria.fr/pipermail/frama-c-discuss)).
-Questions and answers have been cut/pasted with very few editorial
-modifications.
-
-Beware that some of the answers below were given for older versions of
-Frama-C. Some limitations may no longer be present in the current
-version.
-
-# Document history
-
-Created by E. Jenn
-([eric.jenn@fr.thalesgroup.com](mailto:eric.jenn@fr.thalesgroup.com))
-
-Last modified on June 6th 2009 by E. Jenn
-([eric.jenn@fr.thalesgroup.com](mailto:eric.jenn@fr.thalesgroup.com))
-
-## Contributors (by order of apparition)
-
-Claude Marché, Benjamin Monate, David Mentre, Patrick Baudin, Virgile
-Prevosto, Jean-Christophe Filliâtre, Yannick Moy, Jonathan S. Shapiro,
-Pavel Vasilyev, Jianjun Duan, Pascal Cuoq, David Delmas, Stéphane
-Duprat, Jonathan S. Shapiro, Christopher L Conwa, Alan Dunn, Ioana
-Mihaela Geanta, Jens Gerlach, Birger Kollstrand, Claude Marché, Dillon
-Pariente, Nickolay V. Shmyrev, Nicolas Stouls, Christoph Weber,
-Jean-Baptiste Jeannin, Loïc Correnson, Bárbara Vieira, Anne Pacalet,
-Julien Signoles, Jonathan-Christofer Demay, André Passos, Juan Soto,
-Hollas Boris, Guillaume Melquiond, Thomas Pareaud, Rovedy Aparecida
-Busquim e Silva, David Ribeiro Campelo, Omar Chebaro, Vadim Tses’ko,
-Fateh Hettak, Dragan Stosic, François Dupressoir, Kerstin Hartig, Eric
-Jenn, Emilie Timbou
-
-# Further Documentation
-
-## What shall I read first?
-
- - Jessie tutorial at
- <http://frama-c.cea.fr/jessie_tutorial_index.html>
- - Value analysis manual at
- <http://frama-c.cea.fr/download/value-analysis-Beryllium.pdf>
-
-# Question not yet asked / not yet answered
-
-### How are assertions used in the course of a proof?
-
-FIXME
-
-### Some PO is invalid. How can I get a counter example?
-
-FIXME
-
-### How do I read the POs in the gWhy interface? How do they relate to my specification?
-
-FIXME Refer to the Caduceus tool. In particular: The CADUCEUS
-verification tool for C programs by Jean-Christophe Filliâtre et al.
-
-### How can I benefit from the other analyses supported by Frama-C (the value analysis, for instance) to support the deductive verification?
-
-FIXME
-
-### Under Windows, sometimes, I have to stop a prover manually, using the task manager. Is it normal?
-
-This was a problem with older than 2.21 version of the Why platform.
-Later versions should work out of the box.
-
-### Are there any good specification practices (including syntactic ones) to "facilitate" the work of the automated provers?
-
-FIXME
-
-### How do I write sensible loop invariants? What are the questions one shall ask oneself when writing a loop invariant?
-
-FIXME
-
-### I would like to separate the formal specification of my abstract stack from the formal specification of its implementation? Is it possible with ACSL? How do I relate the two specifications in order to prove that the code actually implements an instance of my abstract stack? Do you have any example?
-
-FIXME
-
-### Which companies/institutions/research groups/... has used Frama-C framework successfully?
-
-FIXME
-
-### Has any test been conducted on real applicability of Frama-C framework? (For instance to analyzing or verifying any commercial or open source software)
-
-FIXME
-
-# Methodological questions
-
-### Some PO does not hold or can't be discharged. How do I tackle the problem?
-
-FIXME
-
-### How do I write a good inductive definition? Do you have any good illustrated example?
-
-FIXME
-
-# General questions
-
-### What is the difference between Frama-C and Caduceus?
-
-Frama-C is a platform that allows many techniques to be applied to
-analyse a C program. We are increasingly combining analyses (plugins),
-so that in the end you should be able to prove many properties by
-abstract interpretation, slice the program for the remaining properties
-and prove them by deductive verification inside Why, all automatically.
-Frama-C aims at supporting all of C, which it does already, while
-plugins have their own limitations. The Jessie plugin is the one that
-translates C programs into an intermediate language inside the Why
-platform, so that Frama-C can be used to perform deductive verification
-in the same way as Caduceus. We just started to support casts and unions
-for experiments, but we have not released this part yet. It should be
-the case ultimately that constructs not supported in Caduceus are
-supported in this Jessie plugin.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-October/000594.html>
-
-# Installation
-
-### I can't manage to call the Coq prover from the gWhy interface. What is going on?
-
-This feature was experimental. It shall not be used.
-
-FIXME Explain how to do it another way.
-
-### Can I use another compiler than gcc (e.g., Visual C) ?
-
-Frama-C uses by default cpp to preprocess source files, but you may
-change this by setting option `-cpp-command`. Otherwise, Frama-C relies
-on CIL to link source files and generate a unique abstract syntax tree
-to analyze.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-October/000625.html>
-
-# Value analysis
-
-### Is there implemented any kind of points-to analysis? Which kind?
-
-The values computed by the value analysis can be addresses (for instance
-for the values of pointer variables), so it directly translates into
-points-to information. In the vocabulary that is usual for points-to
-analyses, it is path-sensitive, context-sensitive and interprocedural.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-April/001090.html>
-
-### How are structures and multi-dimensional arrays supported in implemented analysis types? Is the analysis element- and field-aware?
-
-The value analysis is element-aware and field-aware (of course for
-arrays this makes a difference only when the expression used as an index
-can be evaluated with enough precision. There are a number of settings
-to improve precision at the cost of more time and memory use).
-
-In fact, casts between pointers to different structs, and casts between
-pointers to structs and pointers to arrays, are handled with precision
-too.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-April/001090.html>
-
-### Which generic types of analysis are implemented? (Path-sensitive/insensitive, Context-sensitive/insensitive, Inter-procedural/intra-procedural, ...)?
-
-CIL, the front-end on which Frama-C is based, provides generic forward
-and backward generic dataflow analyses that can be used for implementing
-path-sensitive or insensitive, context-sensitive or insensitive, and
-inter- or intra-procedural analyses. The value analysis and other
-analyses such as the functional dependencies computation are implemented
-using these generic analyses, and the simplest of these analyses can be
-used as examples.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-April/001090.html>
-
-# Questions about gWhy
-
-### gWhy highlights are incorrect. why?
-
-Sometimes, code highlighting is incorrect in gWhy.
-
-Under Cygwin, this problem occurs when end of lines are coded with CR/LF
-(DOS). To get correct code highlighting, you have to convert DOS
-end-of-lines to Unix end-of-lines. This can be achieved by means of the
-text editor or by means of dedicated utilities, such as dos2unix for
-instance.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-March/001009.html>
-
-### What is the semantics of gWhy's icons?
-
-The meaning of the icons is the following:
-
- - valid (green dot): the VC is a true formula
- - invalid (red dot): the VC is not a true formula. In principle,
- invalid should be identified with unknown, because provers can very
- rarely say that a formula is definitely not true. Historically,
- Simplify answers is either valid or invalid, where invalid indeed
- means unknown. The GWhy maps those invalid to the question mark but
- the textual output might still classified them as invalid.
- - unknown (question mark) : it is not known if the formula is true or
- not
- - timeout (scissor): the prover did not answer before the timeout (10
- s by default)
- - failure (tools): the prover answer was not recognized. Failure might
- have many causes: failure to run the prover's process, a syntax
- error in the output file, etc. In case of failure, one can inspect
- the problem by activating debug (menu Proof/Debug mode) and look at
- the debugging output in the console.
- - (hard disk): this VC is already known valid in GWhy cache. Note that
- the cache feature is not really used: the VCs in cache are still
- rerun in provers.
-
-Finally, be aware that the actual shape of the icons may vary among
-users because they are built-in GTK icons, which depend on the current
-gtk theme.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-March/001026.html>
-
-# ACSL and Jessie
-
-### Where can I find the latest specification of ACSL?
-
-The latest release of the ACSL specification can be found at
-<http://www.frama-c.cea.fr/acsl.html>
-
-### Does Jessie checks the completeness of behaviors ?
-
-No, not as of version Lithium.
-
-### What is the subset of ACSL implemented in Frama-C, in plugin X or Y ??
-
- - ACSL is a language whose specification is given by the document
- available on <http://frama-c.cea.fr/acsl.html>
- - Frama-C in its current state supports only parts of ACSL. These
- parts are documented in the acsl-implementation.pdf documentation.
- Each acsl-implementation.pdf is specific to the version of Frama-C
- with which it is distributed. The semantics of the revision bars and
- colors is given in the preamble of the document.
- - The next release will come with a Changelog explaining the
- increments. At this time ACSL support of Frama-C is not yet frozen.
- - Plug-ins shall provide documentation describing what part of ACSL
- they can understand. For instance, for Jessie, this information is
- in Jessie's manual (<http://frama-c.cea.fr/jessie.html> ), in
- section 7.2 Unsupported features.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-October/000681.html>
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-May/001155.html>
-
-### Are access structure field using pointer arithmetic and cast supported in Frama-c/Jessie ?
-
-Pointer arithmetic is supported but pointer casts are not (casts between
-primitive types such as int, long, float, etc. are supported, though).
-
-Note that Frama-c itself has very few intrinsic limitations, and for
-instance, the value analysis that constitutes one of the many other
-plug-ins in Frama-C allows heterogeneous pointer casts, such as casts
-from pointer to structure to pointer to basic type, and arbitrary
-pointer arithmetic.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-July/thread.html>
-
-### How do I refer to a global variable « masked » by an argument ?
-
-``` c
-typedef struct { int a; } las;
-
-las * p;
-
-/*@
-requires \valid(p)
-assigns p->a
-*/
-void f() { p->a = 5; }
-
-/*@
-assigns p->a
-*/
-void g(int * p) { f(); }
-```
-
-In the assigns clause of g(), parameter p refers to g()'s argument, not
-to the global variable p.
-
-This problem can be circumvented using ghost variables.
-
-``` c
-typedef struct { int a; } las;
-
-las * p;
-
-//@ghost las ** const PP=&p;
-
-/*@
-requires \valid(p)
-assigns p->a
-@*/
-
-void f() { p->a = 5; }
-
-/*@
-assigns *PP->a
-@*/
-
-void g(int * p) { f(); }
-```
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-April/000564.html>
-
-### How to declare that a returned argument is non null ?
-
-Say you want to express that some function parameters and returns are
-non-null.
-
-First define a non-null predicate:
-
-``` c
-//@ predicate non_null(void *p) = p != 0;
-```
-
-Then, define a declspec of the same name, usually through a macro:
-
-``` c
-#define NON_NULL __declspec(non_null)
-```
-
-Finally, decorate function parameters and returns with the appropriate
-declspec\! The corresponding proposition gets added to the function
-precondition for parameters, and to the function postcondition for
-returns:
-
-``` c
-char*NON_NULL f(char *NON_NULL x, char *y) {
-
-//@ assert x != 0;
-
-//@ assert y != 0;
-
-return x;
-
-}
-```
-
-In the example above, 2 of 3 VC are automatically proved. The last one
-is not provable of course (y \!= 0).
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-October/000598.html>
-
-### What is the meaning of \\valid(a+(low..high)) when low \> high?
-
-\\valid tells something about all the elements of a set of pointers. If
-this set is empty, the property trivially holds. See [this
-discussion](/assets/dokuwiki/issue/156) for more details.
-
-### How can I express properties on arguments and returns with parameters?
-
-For instance, one can express that integer parameters and returns fit in
-a specific range like that:
-
-``` c
-//@ predicate range(integer i, integer lb, integer rb) = lb <= i <= rb;
-
-#define RANGE(a,b) __declspec(range(a,b))
-
-int RANGE(-5,15) f (int RANGE(0,5) x, int RANGE(-5,10) y) {
-
-//@ assert 0 <= x <= 5;
-
-//@ assert -5 <= y <= 10;
-
-return x + y;
-
-}
-```
-
-For those constructs that are not predicates, Jessie prolog defines
-specific declspec:
-
-``` c
-#define FRAMA_C_PTR __declspec(valid)
-
-#define FRAMA_C_ARRAY(n) __declspec(valid_range(0,n))
-```
-
-and an annotation for strings that could be defined in user code but is
-better defined in the prolog because it is useful for everybody:
-
-``` c
-#define FRAMA_C_STRING __declspec(valid_string)
-```
-
-So that one can specify a function like this:
-
-``` c
-char * FRAMA_C_ARRAY(n-1) FRAMA_C_STRING
- my_string_copy (char *FRAMA_C_ARRAY(n-1) dest,
- const char *FRAMA_C_STRING src,
- unsigned n)
-{
-// ...
-return dest;
-}
-```
-
-Fom
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-October/000620.html>
-
-### What about separated clauses?
-
-In the following example the preservation of the loop invariant doesn't
-work, why?
-
-``` c
-/*@
-requires 0 < n;
-requires \valid_range(a, 0, n-1) && \valid_range(b, 0, n-1);
-ensures \forall int k; 0 <= k < n ==> a[k] == b[k];
-*/
-void array_cpy(int* a, int n, int* b)
-{
-/*@ loop invariant 0 <= i <= n &&
- \forall int m; 0 <= m < i ==> a[m] == b[m];
-*/
-for(int i = 0;i< n;i++){
- a[i]=b[i];
- }
-}
-```
-
-Actually, in that case, one must take into account the fact that arrays
-a and b might overlap, such as if you call array\_cpy as
-
-``` c
-array_cpy(t,10,t+1);
-```
-
-One may use the \<\<separated\>\> clause to explicitly state that
-variable a and b in the previous example do not overlap :
-
-``` c
-requires \forall int i,j; \separated(a+i, b+j);
-```
-
-or, simpler:
-
-``` c
-//@ requires \separated(a+(..),b+(..));
-```
-
-Another way :
-
-``` c
-/*@ predicate disjoint_arrays(char *a, char *b, integer i) =
-@ \forall integer k1, k2;
-@ 0 <= k1 < i && 0 <= k2 < i ==> a + k1 != b + k2;
-@*/
-```
-
-Note that in Jessie, separation of pointers into different regions is
-automatic.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-October/000623.html>
-
-### Will assigns \\nothing ensure that nothing has been altered?
-
-Almost\! It ensures that all global variables and memory locations that
-(1) were allocated in the pre-state and (2) do not belong to the set of
-assigned globals and memory locations have the same value in the
-post-state than in the pre-state. This does not prevent their value from
-being modified during the call and then restored.
-
-### Will assigns \<something\> ensure that nothing else has been altered?
-
-Yes (see previous question).
-
-### Is it possible to refer to an array (not the elements of the array) in Pre state after the termination of a function?
-
-Something like:
-
-``` c
-/*@
-
-...
-ensures is_permutation (a, \old_range(a));
-*/
-```
-
-You can mention any term inside construct \\old, with the meaning that
-implicit parts of the states to interpret this term will be taken from
-the pre-state. What you need is a bit more complex, it requires that a
-predicate takes into two states, so that some of its sub-terms are
-evaluated in one state, and others sub terms in another state.
-
-This can be achieved as follows:
-
-``` c
-/*@ predicate is_permutation{S1,S2}(int *a, int *b, int s) =
-@ \forall integer k;
-@ 0 <= k < s ==> \at(a[k],S1) == \at(a[k],S2);
-@*/
-
-/*@ ensures is_permutation{Here,Old}(a,a,s);
-@ */
-void permut(int *a, int s);
-```
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-October/000692.html>
-
-### How do I state that pointers belong to the same block?
-
-Equality of pointer values in C is not the same as equality of the logic
-pointer entities in our memory model. Thus, stating that two pointers
-`first` and `last` are such that `first <= las` in a precondition does
-not guarantee that first and last belong to the same block, which might
-be later on needed to prove the loop invariant. Thus, you must state in
-the precondition and the loop invariant that some pointers belong to the
-same allocated block of memory.
-
-Thus, your example with new annotations looks like:
-
-``` c
-/*@
-@requires \valid_range(first, 0, last-first -1)
-@ && first <= last && \base_addr(first) == \base_addr(last);
-@behavior is_not_empty:
-@ ensures \forall integer i;
-@ 0 <= i < last-first ==> first[i] == value;
-*/
-void fill (int* first, int* last, int value )
-{
-int* it = first;
-/*@
-@loop invariant first <= it <= last
-@ && \base_addr(first) == \base_addr(it)
-@ && \base_addr(last) == \base_addr(it);
-@loop invariant \forall integer k; 0 <= k < it - first ==>
- first[k] == value;
-*/
-while (it != last)
-*it++ = value;
-}
-```
-
-### What about unions and casts?
-
-Unions without pointer fields are now translated to bitvectors, so that
-accesses in these unions are translated to low-level accesses. Thus, the
-following code can be analyzed, but we do not yet provide a way to prove
-the resulting assertions, by asserting that any subset of bits from the
-bitvector representation of 0 is 0:
-
-``` c
-union U {
-int i;
-struct { short s1; short s2; } s;
-};
-
-//@ requires \valid(x);
-void zero(union U* x) {
-x->i = 0;
-//@ assert x->s.s1 == 0;
-//@ assert x->s.s2 == 0;
-}
-```
-
-Unions with pointer fields (either direct fields or sub-fields of
-structure fields) are translated differently, because we treat pointers
-differently than other types, to allow an automatic analysis of
-separation of memory blocks. Thus, we treat unions with pointer fields
-as discriminated unions,
-
-so that writing in a field erases all information on other fields. This
-allows to verify the following program:
-
-``` c
-union U {
-int i;
-int* p;
-};
-
-//@ requires \valid(x);
-void zero(union U* x) {
-x->i = 0;
-//@ assert x->i == 0;
-x->p = (int*)malloc(sizeof(int));
-*x->p = 1;
-//@ assert *x->p == 1;
-}
-```
-
-Finally, casts between pointer types are allowed, with the corresponding
-accesses to memory treated as low-level accesses to some bitvector. This
-allows verifying the safety of the following program:
-
-``` c
-//@ requires \valid(x);
-
-void zero(int* x) {
-char *c = (char*)x;
-*c = 0;
-c++;
-*c = 0;
-c++;
-*c = 0;
-c++;
-*c = 0;
-}
-```
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-November/000789.html>
-
-### On \\base\_addr
-
-Consider the following declarations:
-
-``` c
-struct X {
-int b[4];
-};
-
-X x[5];
-```
-
-What is then the value of \\base\_addr(&(x\[2\].b\[1\])) ?
-
-Is it &(x\[2\].b\[0\]) ( which I think is equal to x+2) or
-&(x\[0\].b\[0\]) (which I think is equal to x) ?
-
-It is the latter. &(x\[2\].b\[0\]) and &(x\[0\].b\[0\]) are both offsets
-of the same base address.
-
-Each plug-in may, however, choose whether to allow to go from
-&(x\[0\].b\[0\]) to &(x\[2\].b\[0\]) using the arithmetic of pointers to
-int (a plug-in may even let the user toggle between both modes with an
-option). If a plug-in chooses to disallow these kinds of "overflows", it
-will generate an unprovable verification condition for a program that
-purposefully accesses one of these addresses as an offset from the
-other, so the soundness of the framework is not in question here.
-
-Consider for instance the (perhaps insufficiently documented)
--unsafe-arrays option for the value analysis. With this option enabled,
-the memory access x\[0\].b\[10\] falls at x\[2\].b\[2\]. Without it, it
-is guaranteed not to fall outside of x\[0\], but it generates a
-condition verification equivalent to "false" (here, something like "10
-\< 4").
-
-### What kind of "post installation" tweaking shall I do to be able to use Coq with Why?
-
-If for some reason (Coq was not installed or its standard library was
-installed in a place which was not writable) Why is not able to put the
-Coq files containing its own prelude in a place where Coq can find them
-by default, it installs them with the other Frama-C files. Adding the
-option -I \`frama-c -print-path\`/why/coq to the coqc/coqide/coqtop
-command line should help.
-
-Please refer to:
-
-1. Yannick Moy's PhD thesis, defended last January:
- <http://www.lri.fr/~marche/moy09phd.pdf>
-2. Lecture notes and exercices for Krakatoa's lecture given at the
- FVOOS Winter school: <http://krakatoa.lri.fr/ws>
-
-### How do Frama-C handles functions without explicit contract? What does warning message No code for function xxxxxx, default assigns generated" mean?
-
-Frama-C generates message
-
-No code for function xxxxxx, default assigns generated
-
-when a function has no explicit assign clause.
-
-This warning says that Frama-C's kernel is generating an assigns clause
-based on the function prototype, because supposing that every location
-in the heap might be changed by a function call would prevent the
-analyses saying something useful. The issue is that this generated
-clause is not guaranteed to be correct. For instance, given the
-prototype void f(int\* x,int l), there's no way to know if x is a
-pointer to a single int (which could be assigned I for instance), or to
-a block of several ints (whose length could be I for instance). It is
-thus important to review the generated clauses (e.g. with the -print
-option. They are also visible in the GUI), or better to give an
-appropriate contract to each prototype which has no associated
-definition.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-March/000936.html>
-
-Note that the previous message is issued for each prototype, regardless
-of whether it has an associated contract with assigns clause for each
-behavior or not, but no assigns clause is generated where the user has
-already provided one.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-March/000947.html>
-
-### Is there any formal specification of standard library functions?
-
-Frama-C is not shipped with a formal specification of standard library
-functions, except for strings functions which can be found in
-jessie\_prolog.h file.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-March/000941.html>
-
-A full C standard library is being developed and will be available in a
-future version of Frama-C
-
-### What is the purpose of behaviors, how do I write correct assume clauses?
-
-The behavior clause has been designed to distinguish different cases in
-the pre state, not in the post state.
-
-Fom
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-March/000948.html>
-
-### How do I specify that a function does not terminate? What is the difference between "ensures \\false;" and "terminates \\false;" ?
-
-Clause "ensures \\false;" is a specification that can only be satisfied
-by a function that does not terminate.
-
-Clause "terminates \\false;" is a specification that can be satisfied by
-any function, since it only means that the function does not have to
-terminate.
-
-### Why does Jessie assume that different pointers points to different memory areas?
-
-Assuming that pointer arguments point to different regions simplifies
-all the pre-conditions that are computed for the function.
-
-Consider
-
-``` c
-int x, y, t[3];
-
-...
-
-void f(int *p, int *q)
-{
-*p = x;
-*q = y;
-//@ assert *p == t[1] ;
-}
-```
-
-If you assume that everything is separated (and in particular that p and
-q point to separate memory regions), the weakest pre-condition for the
-assertion is exactly (I think) "x == t\[1\]". But in order to get this
-very simple pre-condition, you have assumed that p was separate from q,
-and that q was separate from t+1, and also separate from \&p. You also
-assumed that p did not point to itself (that is, that p was separate
-from \&p). In fact there are so many assumptions that I am not sure I am
-not forgetting one here.
-
-Without these assumptions, there would be many more ways the assertion
-could be true. The ACSL formula of the weakest pre-condition for the
-assertion would be one very large disjunction with a lot of cases. The
-sub-formula for "everything is separated and x == t\[1\]" would be only
-one particular way in which the assertion could hold. Another would be
-for instance "q point to p and y is the address of a memory cell with
-contents identical to t\[1\]". There are countless others, and I won't
-even start to enumerate the possibilities when the memory model allows p
-or q to contains addresses such as `(int*)( (char*)t+3)`.
-
-So you can see now how separating assumptions simplifies the properties
-manipulated by Jessie, and consequently the automatic proof of these
-properties.
-
-I think, but then I am not a Jessie specialist, that some of the
-separation assumptions that are made come with Jessie's memory model
-(i.e. they are not optional).
-
-I am thinking for instance of the "p separated from \&p" assumption.
-
-A program where the pointer to int p could receive the address of p (an
-int \*\*) could not be analyzed at all with Jessie, as per section 7.2.1
-of Jessie's reference manual.
-
-Some others separation assumptions, such as "q separated from t+1", are
-made by default, but Jessie is also able not to make these assumptions.
-
-Chapter 5 of Jessie's documentation seems to document this mode (option
--jessie-no-regions). In fact, the only way I can make sense of this
-chapter is if the sentence "Now, function max should only be called ..."
-means "Now let us assume that you did not pass this option. Then,
-function max ...", so it documents it briefly.
-
-But anyway, you need as many separation hypotheses as possible for the
-kind of analysis that a plug-in like Jessie does. Even though option
--jessie-no-region only relaxes some of the separation hypotheses that
-are made by Jessie, the computed weakest preconditions are likely to
-become intractable on many interesting functions when it is enabled,
-independently of whether the function is supposed to work when its
-pointer arguments are aliased.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-January/000912.html>
-
-### Why does this simple example involving floating point number can't be proved?
-
-First, one has to keep in mind that by default, the Jessie interprets
-floats by mathematical real numbers. This might change later, but for
-the moment the default is such because true floating-point support is
-not fully operational.
-
-Let's consider the following example:
-
-``` c
-/*@
-assigns \nothing;
-ensures E < A ==> \result == B;
-*/
-
-float F(float E, float A, float B)
-{
-if (E < A) return B;
-else return 0.;
-}
-```
-
-We have to think of E, A, B as real numbers. The VC for the else branch
-has the form E \>= A (\* for the negation of the test \*) implies the
-post-condition which is of the form E \< A ==\> some P
-
-In principle, this seems trivial because P must be proved under
-contradictory hypotheses E \>= A and E \< A. The point is that here \>=
-and \< denote comparisons of real numbers, and for Simplify and
-Alt-Ergo, the support for real numbers is void or very weak, in the
-sense that they do not even know that \>= is the negation of \<.
-
-The authors of Alt-Ergo are certainly willing to improve their tool. We
-can hope for a better Alt-Ergo in the future.
-
-On the other hand, Simplify will not evolve anymore so it will never
-support real numbers.
-
-Let's consider a second example:
-
-``` c
-/*@
-ensures \result >= 0.0;
-*/
-double sqr(double x)
-{
-return x * x;
-}
-```
-
-Jessie is not able to prove the post-condition. Why?
-
-1. A lot of work has been done on floating-point operations since the
- last release. That is to say, support for floating-point operations
- will be much less partial in the next release than in Lithium, both
- for Jessie and for the Value Analysis.
-2. With the value analysis you need to indicate that the property must
- be analyzed by case by adding an assertion x\<=0 || x\>=0, which
- does not incur any additional proof obligation since it can be
- verified to hold easily. The same trick may help automatic theorem
- provers, if you somehow arrange for this disjunction to be in the
- hypotheses, they may have the idea to study what that means for x\*x
- separately.
-3. With both Jessie or the Value Analysis you will get a proof
- obligation. You will probably want to use the "strict" model in
- which infinites and NaN are treated as unwanted errors when they
- occur. In this case the proof obligation is that x\*x should not
- overflow. So, in the previous example, even with the full model in
- Jessie your post-condition does not hold because NaN is not \>=0
- (the result can be NaN when the sqr function is applied to NaN).
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-May/001162.html>
-
-### How do I verify a recursive function?
-
-Here is a way to verify both the termination and some functional
-property of a recursive function in Frama-C (Lithium) with the Jessie
-plug-in.
-
-This example emphasizes a few current limitations that you should be
-aware. These are planned to be supported in the future.
-
- - decreases clauses not yet supported
- - \\prod construct not yet supported
-
-Moreover, it is worth noting that this code might produce arithmetic
-overflow for large values of n, and this is checked by default.
-
-The following annotated code that is 100% proved, automatically (at
-least with Alt-Ergo and Simplify):
-
-``` c
-// the following pragma allows to ignore potential arithmetic overflow
-
-#pragma JessieIntegerModel(exact)
-
-/* the \prod ACSL construct is not yet supported by the Jessie plugin
- * the following inductive definition is a work-around
- */
-
-// is_prod(a,b,n) true whenever n = prod_{i=a..b} i
-
-/*@ inductive is_prod(integer a, integer b, integer n) {
- @ case is_prod_empty :
- @ \forall integer a,b; a > b ==> is_prod(a,b,1);
- @ case is_prod_left :
- @ \forall integer a,b,n; a <= b && is_prod(a,b-1,n)
- @ ==> is_prod(a,b,b*n);
- @ }
- @*/
-
-/*@ requires n >= 0;
- @ ensures is_prod(1,n,\result);
- @ decreases n; // not yet supported by Jessie plugin
- @*/
-int fact(int n) {
-if (n == 0) return 1;
-// simulating the VC for the decreases clause
-//@ assert 0 <= n && n-1 < n;
-return n * fact(n-1);
-}
-```
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-March/000985.html>
-
-### Shall I use int or integer in my annotations?
-
-Use integer.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-March/001017.html>
-
-### Why are my \#defined symbols not recognized in my annotations?
-
-Let's consider the following two files:
-
-``` f.h
-#define vx 0.0
-```
-
-``` f.c
-#include "f.h"
-float main(float v) { /*@ assert v<=vx ; */ return v; }
-```
-
-The output of Frama-c is the following:
-
- [preprocessing] running gcc -C -E -I. e1.c
- File e1.c, line 6, characters 14-16:
- Error during analysis of annotation: unbound logic variable vx
- e1.c:6: Warning: ignoring logic code annotation
-
-To make \#defined symbols recognized by Frama-C, use the -pp-annot
-switch.
-
-### No prover manage to prove this simple assign clause Is this a bug?
-
-Let's consider the following example:
-
-``` c
-/*@ requires \valid(a+ (0..aLength-1));
- assigns a[..];
-*/
-void foo(int a[], int aLength) {
-int j;
-//@ loop invariant 0 <= j;
-for(j=0; j<aLength; j++) {
- a[j] = 0;
- }
-}
-```
-
-To prove the assign clause, one would need to add a loop assign clause
-which is not yet supported by Jessie (even though it is parsed).
-
-Actually, the "assigns" clause should be implicitly copied to inner
-loops. Both explicit loop assigns clauses, and implicit copy of the main
-assigns to loops will work in next release (post Lithium).
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-April/001044.html>
-
-### How do I verify an axiomatization?
-
-(Some interesting (and funny) comments are provided here:
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-April/001067.html>
-).
-
-A possibility is to express the axiomatization in Coq.
-
-A quicker possibility is first to try to prove
-
-``` c
-//@ lemma l : 0=1;
-```
-
-from your axiomatization.
-
-If it is proven, then yes surely you have to investigate you
-axiomatization. A way to do it then is to remove parts of it until you
-discovered the next subset of axioms that can derive false.
-
-And if the lemma is not proven, then you might also try to prove
-
-``` c
-//@ assert 0=1;
-```
-
-just before return statement of the function that should not be proved
-so quickly. And then proceed the same to remove some part of
-axiomatization.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-April/001070.html>
-
-Complementary information can be found here:
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-April/001073.html>
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-April/001073.html>
-
-### What C/C++ standards are supported by the parser being used in Frama-C? (C89, C99, C++ 2003, GNU Extensions,...)?
-
-Frama-C handles most of C99 (as far as I remember, only the complex type
-defined in C99 is not handled), and most of GCC and MSVC extensions.
-Work has been done on C++ support but is not available. The reason is
-that supporting C++ is a huge amount of work and that not all C++
-constructs are handled yet.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-April/001090.html>
-
-### How to I write assign clauses for multidimensional arrays?
-
-Multidimensional arrays are not yet supported by Jessie.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-May/001165.html>
-
-# On the memory model
-
-### What is the memory model used by Frama-C?
-
-There is not a single memory model. Each plug-in is free to define the
-hypotheses it needs. The annotation language, ACSL, is as
-memory-model-agnostic as we were able to make it.
-
-Basically, there is one untyped byte array for each "base address", base
-addresses being among other things string literals and variables. A
-weakest precondition plug-in such as Jessie may have a more abstract
-view of memory, in order to obtain separation hypotheses between
-pointers of different types for free (at the cost of not handling some
-kinds of pointer casts).
-
-More precisely, the "default" memory model in Jessie is typed, which
-allows to assume separation properties which are handy in general, but
-does not allow pointer casts. When pointer casts occurs, it tries to
-switch to a more complicated memory model.
-
-More details can be found in <http://www.lri.fr/~marche/moy09phd.pdf>.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-May/001190.html>
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-May/001192.html>
-
-### Can the memory model be changed/reimplemented or is it fixed in the core?
-
-Each plug-in is free to represent memory as it sees fit, there is not a
-single representation imposed (or even provided) by the core. What you
-should consider if you are thinking of starting a new plug-in is:
-
- - How will ACSL properties, that are usually attached to a point in
- the analyzed program, translate in your memory model?
-
-<!-- end list -->
-
- - If you plan to interact with existing plug-ins more directly than
- through the exchange of ACSL properties, how will you translate the
- datatypes exported by the existing plug-in into your own structures?
-
-The core does not provide ready-made representations for memory but the
-value analysis and the dependencies analysis share the respective
-datatypes that they use internally. You can use these if they fit your
-purpose. They are documented lightly in the "plug-in development guide",
-pages 27 and 58.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-May/001190.html>
-
-### Is pointer arithmetic supported? Are pointer casts supported?
-
-First, answer to this question depends on what one means by
-"Frama-C/Jessie". Frama-C is an analysis framework where each plug-in
-(Jessie is one such plug-in) is free to define its own limitations on
-the subset of C that it handles. Frama-c itself has very few intrinsic
-limitations.
-
-The value analysis allows heterogeneous pointer casts, such as casts
-from pointer to structure to pointer to basic type, and arbitrary
-pointer arithmetic.
-
-Jessie supports pointer arithmetic, casts between primitive types such
-as int, long, float, etc., but not pointer casts.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-July/000582.html>
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-July/000581.html>
-
-### How do I use the valid\_string and strlen predicates? What are the prototypes provided with Frama-C?
-
-You have to include the jessie/string.h file in order to use the
-valid\_string predicate since it is defined here. The C prototypes
-declared there should conform to the C standard, i.e. there should not
-be any clash.
-
-Generally speaking, including headers from the standard library is not
-really advised (except for the macros), since Frama-C won't know
-anything about the function declared there, and thus won't be able to
-tell something meaningful about code which uses them.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-June/001199.html>
-
-### Does frama-C come with any pre-developed specification of some API (e.g., \<string.h\>, etc.?
-
-Besides the jessie/\*.h headers, other functions are available in the
-share directory of Frama-C (option -print-path will give the exact
-location), usually under the form of a prototype with its specification
-and a reference implementation (which is better suited for the value
-analysis plugin).
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-June/001199.html>
-
-(Note: rather than including frama/include/jessie\_prolog.h, use command
-line option -jessie-std-stubs instead.)
-
-# On loop invariants
-
-### What does Jessie do with loop invariants?
-
-When considering a loop, the only thing that Jessie knows of all the
-steps preceding the current ones is the loop invariant. Conversely,
-everything which is not stated in the loop invariant is out of reach.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-June/001197.html>
-
-### Must a loop invariant hold systematically right after termination of a loop?
-
-The semantics of loop invariant in ACSL does not imply that.
-
-Generally speaking, in
-
-``` c
-//@ invariant I;
-while (true) {
-s1;
-if (c) break;
-s2;
-}
-```
-
-Invariant I is asked to be true when entering the loop, and being
-preserved by the sequence
-
-``` c
-s1;
-if (c) break;
-s2;
-```
-
-When the sequence
-
-``` c
-s1;
-if (c) break;
-```
-
-exits the loop, I may be made wrong if there are side-effects in s1 (or
-in c\!)
-
-In other words: loop invariant hold right after termination of a loop
-only if there are no side-effects between the loop start and the exit.
-But otherwise not necessarily... This is why in textbooks you usually
-prefer to assume side-effect free loop conditions...
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-January/000905.html>
-
-### My loop invariant is too weak Why?
-
-Trouble arises when it is not possible to decide if a given location has
-still its old value or has just been assigned a new one, for instance
-when you write to t\[i\] and read from t\[k\] without knowing whether i
-and k are equal or distinct.
-
-``` c
-/*@
-loop invariant 0 <= i <= length;
-loop invariant \forall integer k; 0 <= k < i ==>
-(\at(a[k],Pre) == old_value ==>
-a[k] == new_value);
-*/
-for (; i != length; ++i) {
- if (a[i] == old_value)
- {
- a[i] = new_value;
- }
-}
-```
-
-The effect of a loop step is not sufficiently defined: from the previous
-invariant, we know what happens to the cell which initial value is
-old\_value, but nothing more. We have to tell the Jessie plugin that the
-other cells are left untouched.
-
-There are two ways to do that
-
- - the simplest one is unfortunately not supported by the plug-in yet:
- loop assigns a\[i\]; indicates in ACSL that at each step, only
- a\[i\] might be modified
- - we must thus add an invariant saying that all the cells beyond i
- still have their initial value:
-
-<!-- end list -->
-
-``` c
-loop invariant \forall integer k; i <= k < length ==>
- a[k] == (\at[k],Pre);
-```
-
-### My loop invariant is still too weak Why?
-
-All POs of the following example can't be discharged, why?
-
-``` c
-/*@ predicate disjoint_arrays(int *a, int *b, integer i) =
- @ \forall integer k1, k2;
- @ 0 <= k1 < i && 0 <= k2 < i ==> a + k1 != b + k2;
- @*/
-
-/*@ requires 0 < n;
- @ requires \valid_range(a, 0, n-1) && \valid_range(b, 0, n-1);
- @ requires disjoint_arrays(a, b, n);
- @ ensures \forall int k; 0 <= k < n ==> a[k] == b[k];
- @*/
-void array_cpy(int* a, int n, int* b) {
-/*@ loop invariant 0 <= i <= n;
- @ loop invariant \forall int m; 0 <= m < i ==> a[m] == b[m];
- @*/
-for (int i = 0; i < n; i++)
- a[i] = b[i];
-}
-```
-
-To prove that the value of \[a\] after copying is the same as the value
-of \[b\] before, you need to strengthen the loop invariant as follows,
-to assess that all of \[b\] does not change during the loop.
-
-``` c
-/*@ requires 0 < n;
- @ requires \valid_range(a, 0, n-1) && \valid_range(b, 0, n-1);
- @ requires disjoint_arrays(a, b, n);
- @ ensures \forall int k; 0 <= k < n ==> a[k] == \at(b[k],Pre);
- @*/
-void array_cpy(int* a, int n, int* b) {
-/*@ loop invariant 0 <= i <= n;
- @ loop invariant \forall int m; 0 <= m < n ==> b[m] == \at(b[m],Pre);
- @ loop invariant \forall int m; 0 <= m < i ==> a[m] == b[m];
- @*/
-for (int i = 0; i < n; i++)
- a[i] = b[i];
-}
-```
-
-Note the use of \\at(b\[m\],Pre) and not \\at(b\[m\],Old), since Old
-doesn't mean anything in a loop invariant.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-October/000642.html>
-
-Another example of weak invariant:
-
-``` c
-int* copy_int_array (int* first, int* last, int* result) {
-//@ ghost int* a = first;
-//@ ghost int* b = result;
-//@ ghost int length = last-first;
-/*@
-loop invariant a <= first <= last;
-loop invariant b <= result <= b+length;
-loop invariant \forall integer k; 0 <= k < first-a ==> a[k] == b[k];
-*/
-while (first!=last) *result++ = *first++;
-return result;
-}
-```
-
-In fact, one should relate the value of result and first during looping,
-this is the part
-
-\[result - b == first - a\]
-
-The correct invariant reads now :
-
-``` c
-/*@
-loop invariant a <= first <= last;
-loop invariant result - b == first - a;
-loop invariant b <= result <= b+length;
-loop invariant \forall integer k; 0 <= k < first-a ==> a[k] == b[k];
-*/
-```
-
-### How can I make a loop invariant specific to a given behavior?
-
-You can use :
-
-``` c
-for <behavior_name> : loop invariant <proposition> ;
-```
-
-### Given a piece of C code, would it be possible to infer an invariant at a particular point of a function?
-
-You may be interested in Yannick Moy's article at VMCAI 2008, on the
-subject of inferring probable invariants (that are checked, e.g. through
-automatic theorem proving). Get it from:
-<http://www.lri.fr/~moy/publis.html> (more details can be found in
-Yannick's PhD thesis: <http://www.lri.fr/~marche/moy09phd.pdf>).
-
-His technique relies on abstract interpretation with linear relational
-abstract domains (his implementation in Jessie uses the APRON library).
-What makes his approach interesting is that the variables for which
-relations are inferred are not only the variables of the program but
-also quantities that are implicitly manipulated by the program, such as
-the offset of the current value of a pointer with respect to its
-original value.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-May/thread.html>
-and
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-May/001127.html>
-
-### What are the differences between Jessie's various integer models.
-
-First, refer to Jessie's tutorial, Section 2.2, especially.
-
-As an illustration of the effect of the integer model, consider the
-following example:
-
-``` c
-typedef int T_ID;
-
-typedef struct
-{
-T_ID next;
-} T_ELT;
-
-T_ELT LIST[4];
-
-//
-// Definition of reachability
-//
-
-/*@
-inductive is_reachable{L}(T_ID start_id, T_ID end_id) {
-case is_length_one{L}:
- \forall T_ID alert_id;
- (0 <= alert_id < 4) ==>
- is_reachable(alert_id, alert_id);
-
-case is_path_non_one{L}:
- \forall T_ID start_id, T_ID end_id;
- ((0 <= start_id < 4) && (0 <= end_id < 4)) ==>
- is_reachable(LIST[start_id].next, end_id) ==>
- is_reachable( start_id, end_id);
-}
-@*/
-
-/*@
-requires \valid(LIST+(0..3));
-ensures is_reachable((T_ID)0,(T_ID)1);
-@*/
-void f()
-{
- LIST[0].next = 1;
- LIST[1].next = 2;
- LIST[2].next = 3;
- LIST[3].next = -1;
-}
-```
-
-Using command frama-c -jessie-gui -jessie-analysis, POs for
-post-condition can't be discharged neither by Ergo, nor by Simplify, nor
-by Z3. Then, using option jessie-int-model exact, all Pos are discharged
-What's going on?
-
-Option jessie-int-model is used to select the way Jessie manages
-integers.
-
-Three options:
-
- - exact: abstract integer are used (no limits)
- - modulo: such as C's int type, integer used in specification are
- defined on 32 bits.
- - bounded: describes a modulo integer arithmetic (or saturating or
- trapping or whatever 2-complement arithmetic you can imagine) with
- additional POs proving that the values do not overflow.
-
-Option "exact" removes the conversion predicates required to convert
-integer to C's int. This makes the proof easier. However, the behavior
-is not correct if an overflow can occur.
-
-See next question.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-June/001214.html>
-
-### Is there any sense to prove a program using the exact integer model?
-
-There are really 2 disjoint goals:
-
- - Is my program correct without machine constraints (i.e., using
- abstract Integers)? In that case use option exact.
- - Are abstract values equals to concrete ones in previous PO? If yes,
- that's OK. If not, try again without the exact option.
-
-If a PO is valid with Integers and timeout without, then a manual proof
-can be tried.
-
-The "bounded" integer model (or "strict" depending on the stage) fits
-these two goals quite well. Jessie generates a first set of POs for
-program correctness. These POs are using mathematical integers, hence
-are prover-friendly, presumably. But it also generates a second set of
-POs. These other POs ensure that the abstract values are equal to the
-concrete values, by stating that the computations do not overflow.
-
-Therefore, if a program is proved correct with respect to the "bounded"
-model, it is also correct in real life. (This property is not true for
-the "exact" model.) But some correct real-life programs may falsify some
-POs of the "bounded" model. These specific programs need the "modulo"
-model, but they are hopefully uncommon and most programs can be proven
-correct with the "bounded" model.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-June/001214.html>
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-June/001216.html>
-
-### Could value analysis be helpful?
-
-(followup to the previous question)
-
-If you have a complete application, the value analyzer could take care
-of overflow and emit an alarm each time it can't ensure that no overflow
-occurs.
-
-However, currently, it assumes that all overflows are desired overflows
-that are part of the program's logic, and it continues the analysis with
-a correct superset of the values that can actually be obtained at
-run-time, assuming 2's complement arithmetic and proper configuration of
-the characteristics of the target architecture.
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-June/001215.html>
-
-From
-<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-June/001217.html>
diff --git a/dokuwiki/start.md b/dokuwiki/start.md
index ff2e47480daf547de2091a4179d2f528b991c128..8c64c294b4a5821b104404b330baa27add48b9b5 100644
--- a/dokuwiki/start.md
+++ b/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
diff --git a/dokuwiki/teaching.md b/dokuwiki/teaching.md
index 40ca439a592eb8c77ebada5d84b6c408fdaf94da..08fcfc2e043dbb2c421cc71c6b065a421d5b959f 100644
--- a/dokuwiki/teaching.md
+++ b/dokuwiki/teaching.md
@@ -1,6 +1,6 @@
----
-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)
diff --git a/html/authors.html b/html/authors.html
index 3dca5f61e27d46231a385716a5598b708e357b25..5be85603af12a9a1b0d7ff39c9ba2300fd4e0b93 100755
--- a/html/authors.html
+++ b/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>
diff --git a/html/careers.html b/html/careers.html
index 0b346dc860d7553a8d7a9a0d5dcb4590c09f8992..6a8abdd765c13d8ea495ec3acd45d6f354b8f5cc 100755
--- a/html/careers.html
+++ b/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>
diff --git a/html/contact.html b/html/contact.html
index 3a5bef681d11b5abe626ccb243413b65f96a1f40..772822d06cbffff75e0c568daffbea5662b0126b 100755
--- a/html/contact.html
+++ b/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>
diff --git a/html/get-frama-c.html b/html/get-frama-c.html
index 293ad5fff6db09acee8b23b14fedc3aa8028ab66..7e4360130df3e68798463228811dbcadd2b09c75 100755
--- a/html/get-frama-c.html
+++ b/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 <dir>
-</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 <dir>
+</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>
diff --git a/html/kernel.html b/html/kernel.html
index 72e609c5e20e2724f08843650b14e74fd4eb97f0..42061efa3b5684b7c288149d506ba50b931cbca1 100755
--- a/html/kernel.html
+++ b/html/kernel.html
@@ -3,159 +3,169 @@ 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 %}
-
- <div id="container" class="mainContainer">
- <div class="tabs">
- <div class="wrap">
- <a class="tabLink" href="/html/kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink active" href=
- "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/gui.html">GUI</a>
- </div>
- </div>
-
- <div class="pageKernel pages">
- <div class="bgTextbig">
- Kernel
- </div>
-
- <div class="wrap">
- <p>WIP (TA)</p>
-
- <p>The Frama-C kernel acts as a <em>lingua franca</em> for all <a href=
- "https://framac-staging.eu-staging.kacdn.net/kernel-plugin/">Frama-C plugins</a>. A software analysis platform that
- checks security, verifies requirements, and guarantees trust in C programs.</p>
-
- <p>Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It
- provides its users with a collection of plug-ins that perform static analysis, deductive verification, and testing, for
- safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their
- integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This
- foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its
- industrial achievements.</p>
-
- <p>3.1. Architecture<br>
- The Frama-C platform is written in OCaml [LDF+13], a functional language whose features are very in- teresting for
- implementing program analyzers [CSB+09]. Fig. 2 shows a functional view of the Frama-C plug-in-oriented architecture (`a
- la Eclipse) whose kernel is based on a modified version of CIL [NMRW02]. CIL is a front-end for C that parses ISO C99
- programs into a normalized representation. For instance, loop constructs (for, while, do & while) are given a single
- normalized form, normalized expressions have no side-effects, etc. Frama-C extends CIL to support dedicated source code
- annotations expressed in ACSL (see Section 3.2). This modified CIL front-end produces the C + ACSL abstract syntax tree
- (AST), an abstract view of the program shared among all analyzers. This AST takes into account machine-dependent
- parameters (size of integral types, endianness, etc.) which can easily be modified by the end-user.<br>
- In addition to the AST, the kernel provides several general services for helping plug-in development [SCP13] and
- providing convenient features to Frama-C’s end-user.</p>
-
- <p>• Messages, source code and annotations are uniformly displayed.<br>
- • Parameters and command line options are homogeneously handled.<br>
- • A journal of user actions can be synthesized and replayed afterwards, a useful feature in debugging and qualification
- contexts [Sig14].<br>
- • A safe serialization mechanism [CDS11] allows the user to save results of analyses and reload them later.<br>
- • Projects, presented in Section 3.3, isolate unrelated program representations, and guarantee the integrity<br>
- of analyses.<br>
- • Consistency mechanisms control the collaboration between analyzers (Section 3.4).<br>
- • A visitor mechanism, partly inherited from CIL, facilitates crawling through the AST and writing code transformation
- plug-ins.</p>
-
- <p>Analyzers are developed as separate plug-ins on top of the kernel. Plug-ins are dynamically linked against the kernel
- to offer new analyses, or to modify existing ones. Any plug-in can register new services in a plug-in database stored in
- the kernel, thereby making these services available to all plug-ins.</p>
-
- <p>3.2. ACSL<br>
- Functional properties of C programs can be expressed within Frama-C as ACSL annotations [BFH+13]. ACSL, the ANSI/ISO C
- Specification Language, is a formal specification language inspired by Java’s JML [BCC+05], both being based on the
- notion of function contract introduced by Eiffel [Mey97]. In its most basic form, the specification (or contract) of a
- function states the pre-conditions it requires from its caller and the post- conditions it ensures when returning. Among
- these post-conditions, one kind of clause plays a particular role by saying which memory locations the function assigns,
- i.e. which locations might have a different value between the pre- and the post-state. Conversely, any memory location
- not mentioned in this clause is supposed to be left unmodified by the function.<br>
- Annotations are written in first-order logic, and it is possible to define custom functions and predicates for use in
- annotations together with ACSL built-ins. Indeed, ACSL features its own functions and predicates to describe memory
- states. However, it does not introduce any notion beyond the C standard, leaving each plug-in free to perform its own
- abstractions over the concrete memory layout.</p>
-
- <p>For instance, Fig. 3 provides a formal ACSL specification for a swap function. Informally, swap is supposed to
- exchange the content of two (valid) pointer cells given as argument.<br>
- The first pre-condition states that the two arguments must be valid int pointers, i.e. that dereferencing a or b will not
- produce a run-time error. In addition, the second pre-condition asks that the two locations do not overlap. \valid and
- \separated are two built-in ACSL predicates.<br>
- The assigns clause states that only the locations pointed to by a and b might be modified by a call to swap; any other
- memory location is untouched. Finally, the post-condition says that at the end of the function, *a contains the value
- that was in *b in the pre-state, and vice versa.<br>
- Function contracts can also be structured into behaviors. In addition to the clauses described above, a behavior can be
- guarded by assumes clauses, which specify under which conditions the behavior is activated. This provides a convenient
- way to distinguish various cases under which the function can be called. Behaviors do not need to be either complete (at
- least one behavior is active for any given call) or disjoint (there is at most one behavior active for a given call), but
- this can be stipulated with the appropriate clauses in order to check that the specification is correct in this respect.
- As an example, Fig. 4 presents the specification of a function swap_or_null similar to swap except that it will attempt
- to swap contents only when both pointers are non-null. This corresponds to the behavior not_null, in which case the
- function expects to have valid (in C a non-null pointer is not necessarily valid) and separated pointers and will act as
- above. On the other hand, in the null case, the function does nothing: at least one pointer is null, so the values cannot
- be swapped. We are always in exactly one of these two cases, so null and not_null are clearly complete and disjoint.<br>
- In addition to function specifications, ACSL offers the possibility of writing annotations in the code, in the form of
- assertions, properties that must be true at a given point, or loop invariants, properties that are true for each loop
- step. More precisely, a loop invariant is associated to a for, while, or do & while loop. It must hold when arriving at
- the loop entry for the first time, and must be preserved by a loop step. That is, if we enter the loop body in a state
- that verifies the invariant, then the invariant must hold at the end of the block – except if we exit from the block
- through goto, break or continue. With these two properties, we can then prove by induction that the invariant is true for
- any number of loop steps<br>
- (including 0). As with assigns clauses in function contracts, loop assigns clauses are a particular case of invariant
- that state which memory locations might have been modified since the beginning of the loop (implicitly stating that all
- other locations are not modified by the loop). Loop invariants are required for<br>
- deductive verification (see Section 5).</p>
-
- <p>As an example, Fig. 5 presents a simple for loop initializing the elements of an array, together with its associated
- invariants. The first invariant specifies the bounds of the index of the loop. Note that the invariant uses i<=10,
- while the test in the code is i<10. Indeed, the invariant must be preserved by any step of the loop, including the
- last one, in which i is equal to 10 at the end of the step. The second invariant states that the i-1 first cells of the
- array have been initialized. It is true before entering the loop, as there is no j such that 0<=j<0, so the
- implication is trivially true. Then, if we suppose that the invariant holds at the beginning of a loop step, the step
- will initialize cell i and increment i, so that the invariant is still true af the end of the step. Similarly, the loop
- assigns clause indicates that the loop has potentially modified i and the first i-1 cells of the array. Namely, this is
- true when entering the loop (nothing has been modified), and if we suppose that only i and the beginning of the array has
- been assigned, the next loop step also assigns i and the ith cell, again making the invariant true at the end of the
- step. Loop invariants are not concerned with termination. Instead, termination can be ensured through the special clause
- loop variant. It requires an integer expression that strictly decreases during a loop step, while remaining positive each
- time the loop enters a new iteration. When both these conditions are met, we know that the loop can only be taken a
- finite number of times. An example of variant for the loop in Fig. 5 would be the following: loop variant 10 - i; Each
- plug-in can provide a validity status to any ACSL property and/or generate ACSL annotations. This lets ACSL annotations
- play an important role in the communication between plug-ins, as explained in Section 3.4. 3.3. Projects Frama-C allows a
- user to work on several programs in parallel thanks to the notion of project. A project consistently stores a program
- with all its required information, including results computed by analyzers and their parameters. Several projects may
- coexist in memory at the same time. A non-interference theorem guarantees project partitioning [Sig09]: any modification
- on a value of a project P does not impact a value of another project P′. Such a feature is of particular interest when
- a program transformer such as E-ACSL (Section 7), Aora ̈ı (Section 8), or Slicing (Section 10.1) is used. The result of
- the transformation is a fresh AST that coexists with the original one, making backtracking and comparisons easy. This is
- illustrated in Section 10.2. Another use of projects is to process the same program in different ways – for instance
- with different analysis parameters. 3.4. Collaborations across analyzers In Frama-C, analyzers can interoperate in two
- different ways: either sequentially, by chaining analysis results to perform complex operations; or in parallel, by
- combining partial analysis results into a full program verification. The former consists in using the results of an
- analyzer as input to another one thanks to the plug-in database stored by the Frama-C kernel. Refer to Section 10.1 for
- an illustration of a sequential analysis. The parallel collaboration of analyzers consists in verifying a program by
- heterogeneous means. ACSL is used to this end as a collaborative language: plug-ins generate program annotations, which
- are then vali- dated by other plug-ins. Partial results coming from various plug-ins are integrated by the kernel to
- provide a consolidated status of the validity of all ACSL properties. For instance, when the Value plug-in (Section 4) is
- unable to ensure the validity of a pointer p, it emits an unproved ACSL annotation assert \valid(p). ACSL’s blocking
- semantics states that an execution trace leading to an invalid property stops its execu- tion (see [GGJK08, HMM12,
- CS12]). Thus, Value can assume that p is valid from this program point onwards, since the execution can only continue if
- the assert is valid. The WP plug-in (Section 5) may later be used to prove this hypothesis, or it can be checked at
- runtime by leveraging the E-ACSL plug-in (Section 7). The kernel automatically computes the validity status of each
- program property from the information provided by all analyzers and ensures the correctness of the entire verification
- process. For that, plug-ins can set the local validity status of an ACSL property, together with its set of dependencies.
- Those dependencies can be: • other ACSL properties that are assumed to be true; • the reachability of a statement;
- • some parameters of the plug-in that set a hypothesis over the memory state of the program. With this information, the
- kernel can then compute a consolidated validity status for each ACSL property. [CS12] presents the algorithm that is used
- for that purpose. Its main correctness property can be stated as: “if the consolidated status of a property is computed
- as valid [resp. invalid] by the kernel, then the property is valid [resp. invalid] with respect to ACSL semanticsâ€.
- This algorithm is also complete:“if a property is proven valid [resp. invalid] by at least one analyzer, then its
- computed consolidated status is valid [resp. invalid] as soon as one other analyzer does not prove the contrary, in which
- case the special status ‘inconsistent’ is computed.â€1</p>
-
+
+<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 %}
+
+ <div id="container" class="mainContainer">
+ <div class="tabs">
+ <div class="wrap">
+ <a class="tabLink" href="/html/kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink active" href=
+ "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/gui.html">GUI</a>
+ </div>
+ </div>
+
+ <div class="pageKernel pages">
+ <div class="bgTextbig">
+ Kernel
+ </div>
+
+ <div class="wrap">
+ <p>WIP (TA)</p>
+
+ <p>The Frama-C kernel acts as a <em>lingua franca</em> for all <a href=
+ "https://frama-c.frama-c.com/html/kernel-plugin.html">Frama-C plugins</a>. A software analysis platform that
+ checks security, verifies requirements, and guarantees trust in C programs.</p>
+
+ <p>Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It
+ provides its users with a collection of plug-ins that perform static analysis, deductive verification, and testing, for
+ safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their
+ integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This
+ foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its
+ industrial achievements.</p>
+
+ <h1>Architecture</h1>
+ <p>The Frama-C platform is written in OCaml [LDF+13], a functional language whose features are very in- teresting for
+ implementing program analyzers [CSB+09]. Fig. 2 shows a functional view of the Frama-C plug-in-oriented architecture (Ã
+ la Eclipse) whose kernel is based on a modified version of CIL [NMRW02]. CIL is a front-end for C that parses ISO C99
+ programs into a normalized representation. For instance, loop constructs (for, while, do & while) are given a single
+ normalized form, normalized expressions have no side-effects, etc. Frama-C extends CIL to support dedicated source code
+ annotations expressed in ACSL (see Section 3.2). This modified CIL front-end produces the C + ACSL abstract syntax tree
+ (AST), an abstract view of the program shared among all analyzers. This AST takes into account machine-dependent
+ parameters (size of integral types, endianness, etc.) which can easily be modified by the end-user.<br>
+ In addition to the AST, the kernel provides several general services for helping plug-in development [SCP13] and
+ providing convenient features to Frama-C’s end-user.</p>
+
+ <ul>
+ <li>Messages, source code and annotations are uniformly displayed.</li>
+ <li>Parameters and command line options are homogeneously handled.</li>
+ <li>A journal of user actions can be synthesized and replayed afterwards, a useful feature in debugging and qualification contexts [Sig14].</li>
+ <li>A safe serialization mechanism [CDS11] allows the user to save results of analyses and reload them later.</li>
+ <li>Projects, presented in Section 3.3, isolate unrelated program representations, and guarantee the integrity of analyses.</li>
+ <li>Consistency mechanisms control the collaboration between analyzers (Section 3.4).</li>
+ <li>A visitor mechanism, partly inherited from CIL, facilitates crawling through the AST and writing code transformation plug-ins.</li>
+ </ul>
+
+ <p>Analyzers are developed as separate plug-ins on top of the kernel. Plug-ins are dynamically linked against the kernel
+ to offer new analyses, or to modify existing ones. Any plug-in can register new services in a plug-in database stored in
+ the kernel, thereby making these services available to all plug-ins.</p>
+
+ <h1>ACSL</h1>
+ Functional properties of C programs can be expressed within Frama-C as ACSL annotations [BFH+13]. ACSL, the ANSI/ISO C
+ Specification Language, is a formal specification language inspired by Java’s JML [BCC+05], both being based on the
+ notion of function contract introduced by Eiffel [Mey97]. In its most basic form, the specification (or contract) of a
+ function states the pre-conditions it requires from its caller and the post- conditions it ensures when returning. Among
+ these post-conditions, one kind of clause plays a particular role by saying which memory locations the function assigns,
+ i.e. which locations might have a different value between the pre- and the post-state. Conversely, any memory location
+ not mentioned in this clause is supposed to be left unmodified by the function.<br>
+ Annotations are written in first-order logic, and it is possible to define custom functions and predicates for use in
+ annotations together with ACSL built-ins. Indeed, ACSL features its own functions and predicates to describe memory
+ states. However, it does not introduce any notion beyond the C standard, leaving each plug-in free to perform its own
+ abstractions over the concrete memory layout.</p>
+
+ <p>For instance, Fig. 3 provides a formal ACSL specification for a swap function. Informally, swap is supposed to
+ exchange the content of two (valid) pointer cells given as argument.<br>
+ The first pre-condition states that the two arguments must be valid int pointers, i.e. that dereferencing a or b will not
+ produce a run-time error. In addition, the second pre-condition asks that the two locations do not overlap. \valid and
+ \separated are two built-in ACSL predicates.<br>
+ The assigns clause states that only the locations pointed to by a and b might be modified by a call to swap; any other
+ memory location is untouched. Finally, the post-condition says that at the end of the function, *a contains the value
+ that was in *b in the pre-state, and vice versa.<br>
+ Function contracts can also be structured into behaviors. In addition to the clauses described above, a behavior can be
+ guarded by assumes clauses, which specify under which conditions the behavior is activated. This provides a convenient
+ way to distinguish various cases under which the function can be called. Behaviors do not need to be either complete (at
+ least one behavior is active for any given call) or disjoint (there is at most one behavior active for a given call), but
+ this can be stipulated with the appropriate clauses in order to check that the specification is correct in this respect.
+ As an example, Fig. 4 presents the specification of a function swap_or_null similar to swap except that it will attempt
+ to swap contents only when both pointers are non-null. This corresponds to the behavior not_null, in which case the
+ function expects to have valid (in C a non-null pointer is not necessarily valid) and separated pointers and will act as
+ above. On the other hand, in the null case, the function does nothing: at least one pointer is null, so the values cannot
+ be swapped. We are always in exactly one of these two cases, so null and not_null are clearly complete and disjoint.<br>
+ In addition to function specifications, ACSL offers the possibility of writing annotations in the code, in the form of
+ assertions, properties that must be true at a given point, or loop invariants, properties that are true for each loop
+ step. More precisely, a loop invariant is associated to a for, while, or do & while loop. It must hold when arriving at
+ the loop entry for the first time, and must be preserved by a loop step. That is, if we enter the loop body in a state
+ that verifies the invariant, then the invariant must hold at the end of the block – except if we exit from the block
+ through goto, break or continue. With these two properties, we can then prove by induction that the invariant is true for
+ any number of loop steps<br>
+ (including 0). As with assigns clauses in function contracts, loop assigns clauses are a particular case of invariant
+ that state which memory locations might have been modified since the beginning of the loop (implicitly stating that all
+ other locations are not modified by the loop). Loop invariants are required for<br>
+ deductive verification (see Section 5).</p>
+
+ <p>As an example, Fig. 5 presents a simple for loop initializing the elements of an array, together with its associated
+ invariants. The first invariant specifies the bounds of the index of the loop. Note that the invariant uses i<=10,
+ while the test in the code is i<10. Indeed, the invariant must be preserved by any step of the loop, including the
+ last one, in which i is equal to 10 at the end of the step. The second invariant states that the i-1 first cells of the
+ array have been initialized. It is true before entering the loop, as there is no j such that 0<=j<0, so the
+ implication is trivially true. Then, if we suppose that the invariant holds at the beginning of a loop step, the step
+ will initialize cell i and increment i, so that the invariant is still true af the end of the step. Similarly, the loop
+ assigns clause indicates that the loop has potentially modified i and the first i-1 cells of the array. Namely, this is
+ true when entering the loop (nothing has been modified), and if we suppose that only i and the beginning of the array has
+ been assigned, the next loop step also assigns i and the ith cell, again making the invariant true at the end of the
+ step. Loop invariants are not concerned with termination. Instead, termination can be ensured through the special clause
+ loop variant. It requires an integer expression that strictly decreases during a loop step, while remaining positive each
+ time the loop enters a new iteration. When both these conditions are met, we know that the loop can only be taken a
+ finite number of times. An example of variant for the loop in Fig. 5 would be the following: loop variant 10 - i; Each
+ plug-in can provide a validity status to any ACSL property and/or generate ACSL annotations. This lets ACSL annotations
+ play an important role in the communication between plug-ins, as explained in Section 3.4.</p>
+
+ <h1>Projects</h1>
+ <p>Frama-C allows a
+ user to work on several programs in parallel thanks to the notion of project. A project consistently stores a program
+ with all its required information, including results computed by analyzers and their parameters. Several projects may
+ coexist in memory at the same time. A non-interference theorem guarantees project partitioning [Sig09]: any modification
+ on a value of a project P does not impact a value of another project P′. Such a feature is of particular interest when
+ a program transformer such as E-ACSL (Section 7), Aora ̈ı (Section 8), or Slicing (Section 10.1) is used. The result of
+ the transformation is a fresh AST that coexists with the original one, making backtracking and comparisons easy. This is
+ illustrated in Section 10.2. Another use of projects is to process the same program in different ways – for instance
+ with different analysis parameters.</p>
+
+ <h1>Collaborations across analyzers</h1>
+ In Frama-C, analyzers can interoperate in two
+ different ways: either sequentially, by chaining analysis results to perform complex operations; or in parallel, by
+ combining partial analysis results into a full program verification. The former consists in using the results of an
+ analyzer as input to another one thanks to the plug-in database stored by the Frama-C kernel. Refer to Section 10.1 for
+ an illustration of a sequential analysis. The parallel collaboration of analyzers consists in verifying a program by
+ heterogeneous means. ACSL is used to this end as a collaborative language: plug-ins generate program annotations, which
+ are then vali- dated by other plug-ins. Partial results coming from various plug-ins are integrated by the kernel to
+ provide a consolidated status of the validity of all ACSL properties. For instance, when the Value plug-in (Section 4) is
+ unable to ensure the validity of a pointer p, it emits an unproved ACSL annotation assert \valid(p). ACSL’s blocking
+ semantics states that an execution trace leading to an invalid property stops its execu- tion (see [GGJK08, HMM12,
+ CS12]). Thus, Value can assume that p is valid from this program point onwards, since the execution can only continue if
+ the assert is valid. The WP plug-in (Section 5) may later be used to prove this hypothesis, or it can be checked at
+ runtime by leveraging the E-ACSL plug-in (Section 7). The kernel automatically computes the validity status of each
+ program property from the information provided by all analyzers and ensures the correctness of the entire verification
+ process. For that, plug-ins can set the local validity status of an ACSL property, together with its set of dependencies.
+ Those dependencies can be:</p>
+ <ul>
+ <li>other ACSL properties that are assumed to be true;</li>
+ <li>the reachability of a statement;</li>
+ <li>some parameters of the plug-in that set a hypothesis over the memory state of the program.</li>
+ </ul>
+ <p>With this information, the
+ kernel can then compute a consolidated validity status for each ACSL property. [CS12] presents the algorithm that is used
+ for that purpose. Its main correctness property can be stated as: “if the consolidated status of a property is computed
+ as valid [resp. invalid] by the kernel, then the property is valid [resp. invalid] with respect to ACSL semanticsâ€.
+ This algorithm is also complete:“if a property is proven valid [resp. invalid] by at least one analyzer, then its
+ computed consolidated status is valid [resp. invalid] as soon as one other analyzer does not prove the contrary, in which
+ case the special status ‘inconsistent’ is computed.â€</p>
+
<div class="aboutKernel">
- <h2 class="subTitle">Some articles about kernal sections</h2>
+ <h2 class="subTitle">Some articles about kernel sections</h2>
<div class="kernelSwiper swiper-container">
<div class="swiper-wrapper">
@@ -217,12 +227,12 @@ title: Kernel & Plugins - Frama-C
<div class="swiper-pagination"></div>
</div>
- </div>
- </div>
+ </div>
+ </div>
</div>
- {% include footer.html %}
-
- <div class="clear"></div>
- </div>
- </div>
-</body>
\ No newline at end of file
+ {% include footer.html %}
+
+ <div class="clear"></div>
+ </div>
+ </div>
+</body>
diff --git a/html/terms-of-use.html b/html/terms-of-use.html
index 9949e4f03f081efa5a2a42b27cb6f5559f54804d..2e656e6874513735b3bd7728808b16f3ef9c098f 100755
--- a/html/terms-of-use.html
+++ b/html/terms-of-use.html
@@ -1,64 +1,64 @@
---
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>
diff --git a/html/using-frama-c.html b/html/using-frama-c.html
index a8c57222065e5bbd0de6508190e0961c4527d817..9901cb57ac4a788a6d875fae7e210962cbfd3729 100755
--- a/html/using-frama-c.html
+++ b/html/using-frama-c.html
@@ -1,12 +1,12 @@
---
-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>
diff --git a/index.html b/index.html
index 761543f1bed31959010e31ad1eaacfe4e10b6ccb..b27e400bd5dd2a2d1cb059f9c324bbbe39777741 100755
--- a/index.html
+++ b/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>
\ No newline at end of file
+<body>