User Tools

  • Logged in as: anonymous (anonymous)
  • Logout

Site Tools


mantis:frama-c:frequently_asked_questions

Table of Contents

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

Document history

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

Last modified on June 6th 2009 by E. Jenn (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?

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 ?

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

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:

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

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

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

What about separated clauses?

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

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:

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

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:

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

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

On \base_addr

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

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

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:

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

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

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

Why are my #defined symbols not recognized in my annotations?

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.

No prover manage to prove this simple assign clause Is this a bug?

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

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

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

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?
  • 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

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

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.

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

My loop invariant is still too weak Why?

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

How can I make a loop invariant specific to a given behavior?

You can use :

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:

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

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