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)