--- layout: fc_discuss_archives title: Message 62 from Frama-C-discuss on November 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] definition of \base_addr



Hi,

the definition of \base_addr reads "returns the base address of an  
allocated pointer".
I assume that for global or local variable a of type int a[4] holds:
	\base_addr(&a[3]) = \base_addr(a+3) = \base_addr(a)

But what if we define

struct X {
     int b[4];
};

X x[5];

What is then the value of
	\base_addr(&(x[2].b[1])) ?
Is it
	&(x[2].b[0]) ( which I think is equal to x+2)
or
	&(x[0].b[0]) (which I think is equal to x)
?

Thanks in advance.

Jens