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
- Subject: [Frama-c-discuss] WP plugin / question about address of variable on stack
- From: virgile.prevosto at cea.fr (Virgile Prevosto)
- Date: Mon, 17 Oct 2011 11:13:21 +0200
- In-reply-to: <CAFaEDLAvkH=TkN2d_PEQ15dF7x1HFa-OFccf4SvN1NTOahW8jw@mail.gmail.com>
- References: <CAFaEDLB1ae2J8G9g+WzHUkbrVcLDorhPefaq6d9B8OyO5YEF=Q@mail.gmail.com> <F3E66EEC-D8CA-4E87-9DFD-1A64AF1D5878@first.fraunhofer.de> <CAFaEDLAvkH=TkN2d_PEQ15dF7x1HFa-OFccf4SvN1NTOahW8jw@mail.gmail.com>
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
- Follow-Ups:
- [Frama-c-discuss] WP plugin / question about address of variable on stack
- From: sylvain.nahas at googlemail.com (sylvain nahas)
- [Frama-c-discuss] WP plugin / question about address of variable on stack
- References:
- [Frama-c-discuss] WP plugin / question about address of variable on stack
- From: sylvain.nahas at googlemail.com (sylvain nahas)
- [Frama-c-discuss] WP plugin / question about address of variable on stack
- From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
- [Frama-c-discuss] WP plugin / question about address of variable on stack
- From: sylvain.nahas at googlemail.com (sylvain nahas)
- [Frama-c-discuss] WP plugin / question about address of variable on stack
- Prev by Date: [Frama-c-discuss] WP plugin / question about address of variable on stack
- Next by Date: [Frama-c-discuss] WP plugin / question about address of variable on stack
- Previous by thread: [Frama-c-discuss] WP plugin / question about address of variable on stack
- Next by thread: [Frama-c-discuss] WP plugin / question about address of variable on stack
- Index(es):