--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on October 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP plugin / question about address of variable on stack



Hi,

this is a very helpful response!

May I suggest to put these information in the ACSL documentation,
maybe in the chapter 2.7.1 (Memory blocks and pointer dereferencing)?

Thank you very much, again,
Sylvain

On Mon, Oct 17, 2011 at 11:13 AM, Virgile Prevosto
<virgile.prevosto at cea.fr> wrote:
> 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
>
> _______________________________________________
> 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
>