--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on November 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Documentation of \valid



Thanks for the contribution. However, I disagree with some of your points.
First, it has nothing todo with Jessie. Only ACSL semantics is under 
discussion.
Next, to illustrate my point: look at ACSL doc, section 2.7 where \valid 
is defined.
You see:

----------------
\valid applies to a set of terms of some pointer type. \valid(s) holds if
and only if dereferencing any p in s is safe. In particular, 
\valid(\empty) holds.
--------------

not very precise, I admit, but just after you have:

---------------------
 \offset(p) returns the offset between p and its base address

\offset(p) = (char*)p - \base_addr(p)

the following property holds: for any set of pointers s, \valid(s) if 
and only if for all p in s:

\offset(p) >= 0 && \offset(p) + sizeof(*p) <= \block_length(p)
-------------------------------------

This last formula should be seen as the formal def of \valid(p). It is 
dependent of the C type of p, via the use of sizeof(*p). This def is 
independant of Jessie, and it has nothing to do with the fact that 
jessie use a so-called typed memory model or not.

Now, back to your example, let's do a little test:
-------------------
#include <stdio.h>

struct A {
    int x;
    int y;
};
struct B {
    struct A a;
    int z;
};

typedef int arr3[3];

void f(arr3 t, struct B b) {
  printf("sizeof(int): %ld\n",sizeof(int));
  printf("sizeof(void*): %ld\n",sizeof(void*));
  printf("sizeof(t): %ld\n",sizeof(t));
  printf("sizeof(b): %ld\n",sizeof(b));
  printf("sizeof(*t): %ld\n",sizeof(*t));
}

int main() {
  arr3 t;
  struct B b;
  f(t,b);
  return 0;
}
----------------

What I obtain is

----------------------------
sizeof(int): 4
sizeof(void*): 8
sizeof(t): 8
sizeof(b): 12
sizeof(*t): 4
------------------------

As you can see, the parameter of f is a pointer (size 8, on my 64-bit 
computer), and *t has size 4 (sizeof int).
On the other hand, parameter b has size 12 (for the three ints in that 
structure).

Hence
\valid(t) means that from t, we are given 4 valid bytes
\valid(b) means that from b, we are given 12 valid bytes

That's it! If you want to specify that your have an array of 3 ints from 
t, you need \valid(t+(0..2))

All this comes from the semantics of C itself, which interprets type 
"arr3" in the profile of f as "int*" only

- Claude






Hollas Boris (CR/AEY1) wrote:
> I've added a section on types in the wiki.
>
> _______________________________________________
> 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
>   


-- 
Claude March?                          | tel: +33 1 72 92 59 69           
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93 
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29   
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |