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