--- layout: fc_discuss_archives title: Message 62 from Frama-C-discuss on November 2008 ---
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