--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on October 2011 ---
Hello, On 17/10/2011 10:05, sylvain nahas wrote: > It all depends what a "valid" pointer is for Frama-C. I could not > found a good description, nor the deductive rules used. > Do you have pointers? Basically, \valid(p) holds if and only if *p has a definite semantics according to the C standard (note that it depends on the type with which p is declared: \valid((int *)p) and \valid((char *)p) are two different things). Unfortunately, this cannot really be counted as a good description (it's defined in paragraph 6.5.3.2.4 of said norm and the associated footnote 83, and some hints at what constitutes a valid pointer are scattered throughout the norm). ACSL tries to be a bit more precise without enforcing a particular memory model. Namely, the memory is structured in allocated blocks, who have a base address (either the beginning of a declared object or array, or the pointer returned by a successful call to malloc), and a length (\block_length, the last byte that can be referenced from the base address). ACSL uses then a pretty classical representation for pointers, under the form base_address + offset, and its validity can be expressed as an arithmetic relation over \block_length, \offset and sizeof: - \offset(p)>=0 , i.e. p is bigger than its base address - \offset(p)+sizeof(*p) <= \block_length(\base_addr(p)), i.e. the remainder of the block starting from offset p is large enough to store an object of the desired type Note that this description is not completely accurate still: in particular, it does not take into account potential alignment constraint (i.e. (unsigned long)p % alignof(*p) == 0) null pointer is guaranteed by the standard to always be invalid, so indeed \valid(p) ==> p!=\null; (but of course the reverse is not true, a pointer can be invalid without being null). HTH -- E tutto per oggi, a la prossima volta Virgile