Runtime checking Old Static Variable Accesses

[DavePearce]

The following from StaticVar_Valid_15 is not currently supported:

method inc()
requires var >= 0
ensures old(var) < var:
    var = var + 1

The problem is that, whilst the interpreter copies the entire heap, this does not include any static variables!

[DavePearce]

The plan is to move statics from CallStack into Heap.