Revisit Restrictions on Bounds Expressions

[lenary]

In particular, the following is going to give us code generation problems, because we need to do a bounds check when we dereference p, which would use the bounds we're currently defining:

p : bounds(l, u)

where l or u contain any dereference of p, such as *p, p[i], p.f or p->f