--- layout: fc_discuss_archives title: Message 22 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



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