Is there a way to drop LOCAL variables that are no longer needed in VST?

Question

When working through longer functions when using verifiable-C, it is often the case that LOCAL variables are no longer needed after a certain point. In particular, the C-light translated code often adds many LOCAL variables that are only used briefly.

Is there a tactic or lemma in VST that I can use to discard a LOCAL variable when I know that it will no longer be needed. This can help reduce the clutter in the LOCAL context. I'm also hoping that it will be able to speed up VST as well as I find that it gets slower as my LOCAL context gets bigger and bigger (though the slowdown might be unrelated).

Answer 1

I did try the suggested deadvars! tactic, but when the remaining statements is large, the deadvars! tactic turn out to be quite slow.

However, I did find the drop_LOCALs tactic in the manual, and while using it might be a little less robust, it worked well and improved the memory use of checking my script (a bit less than I had hoped, but it was a definite improvement).

Answer 2

Try the deadvars! tactic. (Look it up in VC.pdf manual, but really, just say deadvars!.