Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie regions

  • Subject: [Frama-c-discuss] Jessie regions
  • From: Pascal.CUOQ at cea.fr (Pascal Cuoq)
  • Date: Tue, 27 Jan 2009 14:32:34 +0100
  • In-reply-to: <7CD088A8-35C2-4166-AACB-C36086BBF58F@first.fraunhofer.de>
  • References: <7CD088A8-35C2-4166-AACB-C36086BBF58F@first.fraunhofer.de>
This message is an answer to an off-list question concerning
>  the rationale behind the decision to assume that
> different pointers (of a function) point to different memory regions?
> Is it because it simplifies proving?

Yes. More precisely, 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 making separation
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.

Pascal

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090127/09769799/attachment.htm