Extend new checking description to lvalues

[dtarditi]

We're revamping the description of checking bounds declarations to handle expressions with control-flow and multiple nested assignments (PR #342). PR #342 handles variables. We need to generalize the description from variables to lvalue expressions. We need to check that assignments to members preserve bounds invariants for structures.