[wp] unsoundness for base-offset

Computation of WP for \offset() in MemTyped is actually using a function base_offset(idx) that max index of cells in memory to their actual offset in bytes. Example:

struct S {
  int f;    // index 0, offset  0
  long g;   // index 1, offset  4
  int h;    // index 2, offset 12
};          // size,=3, sizeof=16

This function is left mostly unspecified, and is required to be monotonic. This prevent WP from computing exact offsets, but is not a problem, this is just an under-specification.

Moreover, the index-offset correspondance could be formally specified for each known base-address from its type (if it does not changed, as it is assumed in MemTyped).

However, this function is currently the same for all base address, which is certainly incorrect and might cause unsoundness when asking WP for computing \offset() within variables of different types.

It shall be modelled as base_offset(base, index).