[gtlc] Garbage Collection and unboxing per data flow proofs

[ayazhafiz]

We can also allocate all heap values at compile-time as globals. But garbage collection is more interesting.