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] 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