--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on November 2009 ---
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 |