Improved reasoning about assignments in loops

[DavePearce]

Currently, the following fails to verify:

int[] items = [1,2,3]
for i in 0..|items|:
   items[i] = 0

assert |items| == 3

However, it is possible to make this verify by adding some additional invariants. Essentially, if items is never used as a direct lval then we need to:

1) Declare variable items$old before loop which holds value on entry. 2) Add invariant of the form invariant (forall i:int :: Array#Length(items) == Array#Length(items$old));

This is pretty easy, though it requires descending all compound structures accordingly. Basically, extract lvals and discard any involving a modified variable or a dereference.

@utting This would be very cute to implement!

[DavePearce]

For records, we have that fields which are not assigned are unchanged. For example, this should verify:

{int f, int g} rec = {f:0, g:1}

for i in 0..n:
   rec.f = rec.f + 1

assert rec.g == 1