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