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



Dear Jens,

>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)
>?

It is the latter. &(x[2].b[0]) and &(x[0].b[0]) are both
offsets of the same base address.

Each plug-in may, however, choose whether to allow to go from 
&(x[0].b[0]) to &(x[2].b[0]) using the arithmetics
of pointers to int (a plug-in may even let the user toggle
between both modes with an option). If a plug-in chooses
to disallow these kinds of "overflows", it will generate
an unprovable verification condition for a program that
purposefully accesses one of these addresses as an offset
from the other, so the soundness of the framework is
not in question here.

Consider for instance the (perhaps unsufficiently documented)
-unsafe-arrays option for the value analysis.
With this option enabled, the memory access x[0].b[10]
falls at x[2].b[2]. Without it, it is guaranteed not to fall
outside of x[0], but it generates a condition verification
equivalent to "false" (here, something like "10 < 4").

Pascal