We have updated the specification of checking of bounds declarations. In the specification, the CheckLValue function infers bounds for the values stored in lvalues (RB, in the specification). In the Checked C implementation, we use the type of the value to infer bounds in some cases. For example, we can infer bounds for Ptr values or array-typed values. The specification needs to be updated to reflect this.