SYSTEM WARNING: 'session_name(): Cannot change session name when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 231

SYSTEM WARNING: 'session_set_cookie_params(): Cannot change session cookie parameters when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 232

- Logged in as: anonymous (anonymous)
- Log Out

mantis:frama-c:frequently_asked_questions

The following questions have been collected on the Frama-C mailing list (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.

Created by E. Jenn (eric.jenn@fr.thalesgroup.com)

Last modified on June 6th 2009 by E. Jenn (eric.jenn@fr.thalesgroup.com)

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

- 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

Refer to the Caduceus tool. In particular: The CADUCEUS verification tool for C programs by Jean-Christophe FilliÃ¢tre et al.

This was a problem with older than 2.21 version of the Why platform. Later versions should work out of the box.

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

This feature was experimental. It shall not be used.

Explain how to do it another way.

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

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

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

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

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

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

The latest release of the ACSL specification can be found at http://www.frama-c.cea.fr/acsl.html

No, not as of version Lithium.

- 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

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

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.

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

Say you want to express that some function parameters and returns are non-null.

First define a non-null predicate:

`//@ predicate non_null(void *p) = p != 0;`

Then, define a declspec of the same name, usually through a macro:

`#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:

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

\valid tells something about all the elements of a set of pointers. If this set is empty, the property trivially holds. See this discussion for more details.

For instance, one can express that integer parameters and returns fit in a specific range like that:

//@ 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:

#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:

`#define FRAMA_C_STRING __declspec(valid_string)`

So that one can specify a function like this:

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

In the following example the preservation of the loop invariant doesn't work, why?

/*@ 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

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 :

requires \forall int i,j; \separated(a+i, b+j);

or, simpler:

`//@ requires \separated(a+(..),b+(..));`

Another way :

```
/*@ 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

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.

Yes (see previous question).

Something like:

```
/*@
...
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:

/*@ 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

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:

/*@ @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; }

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:

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:

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:

//@ 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

Consider the following declarations:

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”).

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:

- Yannick Moy's PhD thesis, defended last January: http://www.lri.fr/~marche/moy09phd.pdf
- Lecture notes and exercices for Krakatoa's lecture given at the FVOOS Winter school: http://krakatoa.lri.fr/ws

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

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

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

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.

Assuming that pointer arguments point to different regions simplifies all the pre-conditions that are computed for the function.

Consider

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

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:

/*@ 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:

/*@ ensures \result >= 0.0; */ double sqr(double x) { return x * x; }

Jessie is not able to prove the post-condition. Why?

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

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):

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

Let's consider the following two files:

- c
#define vx 0.0

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

Let's consider the following example:

/*@ 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

(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

`//@ 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

`//@ 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

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

Multidimensional arrays are not yet supported by Jessie.

From http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-May/001165.html

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

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?

- 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

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

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

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.)

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

The semantics of loop invariant in ACSL does not imply that.

Generally speaking, in

//@ 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

s1; if (c) break; s2;

When the sequence

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

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.

/*@ 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:

loop invariant \forall integer k; i <= k < length ==> a[k] == (\at[k],Pre);

All POs of the following example can't be discharged, why?

/*@ 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.

/*@ 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:

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 :

```
/*@
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];
*/
```

You can use :

for <behavior_name> : loop invariant <proposition> ;

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

First, refer to Jessie's tutorial, Section 2.2, especially.

As an illustration of the effect of the integer model, consider the following example:

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

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

(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

mantis/frama-c/frequently_asked_questions.txt · Last modified: 2012/05/16 14:39 by yakobowski