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