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