Simplify description of checking of bounds declarations.

[dtarditi]

Currently we are using a notion of pending variables in the description of checking of bounds declarations. They are computed by another function that is called during checking. This doesn't extend well to lvalue expressions because lvalue expressions depend on variables, which may be modified within an expression.

An alternative is to replace pending variables with read/write summaries. We can then determine if the read/write summary for expression with an unspecified order of evaluation with respect to each other conflict. The read/write summaries for lvalue expressions can use variables defined in known frames of reference (states after an expression is evaluated).