Add frame suppression to microcode?

[MattWindsor91]

One way of dealing with referential transparency might be to add a new action

forget LVALUE

into the Microcode representation used in the post-array Starling command semantics. The semantics of this action would be to prevent LVALUE from being framed, but not assign it to a value.

Thus, if we add custom command semantics, symbolic commands that affect a heap can now be represented as e.g. (in aspirational Starling syntax, I'll propose this in a later issue):

command Lock(shared int &heap, thread int lockID)
{
    forget heap, %{Lock(#1)}(lockID)
} 

This generalises #81.

[septract]

Just to note that forget is a command in the v popular Boogie intermediate verification language (where it's called havoc). Perhaps this suggests it's a good choice? See the Boogie reference manual, S9.4:

[MattWindsor91]

This is done now, I believe.