Frama-C-discuss mailing list archives

Christoph.Weber at first.fraunhofer.de (Christoph Weber) · Mon, 9 Mar 2009 09:36:56 +0100

Hello,

referring the discussion regarding disjoint memory regions:

I want to know, whether the built-in assumption that all memory regions are disjoint is a mere assumption or a precondition, which is enforced during evaluation.

I hope my question is clear enough, if not I will try to clarify it.

Sincerely

Christoph
  ----- Original Message ----- 
  From: Pascal Cuoq 
  To: Jens Gerlach 
  Cc: Frama-C public discussion 
  Sent: Tuesday, January 27, 2009 2:32 PM
  Subject: Re: [Frama-c-discuss] Jessie regions

  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

------------------------------------------------------------------------------

  _______________________________________________
  Frama-c-discuss mailing list
  Frama-c-discuss at lists.gforge.inria.fr
  http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090309/fbce5ae0/attachment.htm 