Skip to content
Snippets Groups Projects
Commit a7405dac authored by Augustin Lemesle's avatar Augustin Lemesle
Browse files

Merge branch 'feature/wiki' into 'master' 

Documentation pages

See merge request frama-c/frama-c.frama-c.com!10
parents 0de8dadb 9651209f
No related branches found
No related tags found
1 merge request!10Documentation pages
Pipeline #23470 passed
Stage: deploy
Hide whitespace changes
Inline Side-by-side
dokuwiki/external_plugins.md
+ 25
− 4
View file @ a7405dac
---
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
......
dokuwiki/faq.md deleted 100644 → 0
+ 0
− 178
View file @ 0de8dadb
---
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).
dokuwiki/frequently_asked_questions.md deleted 100644 → 0
+ 0
− 1486
View file @ 0de8dadb
---
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>
dokuwiki/start.md
+ 49
− 24
View file @ a7405dac
......@@ -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
......
dokuwiki/teaching.md
+ 3
− 9
View file @ a7405dac
---
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)
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment