SV-Comp: Fix unsoundness in MemSafety category caused by limitations due to scope #1199
Description
One issue with competing in the MemSafety category of SV-COMP (c.f. PRs #1197 #1179 #1139 #1127 #1123 #1114 #1099 #1094 #1050 ) is that our frontend pulls up all declarations to the top-level scope.
This transformation turns code that has Undefined Behavior into code without any UB, which is of course perfectly ok for a compiler to do, but bad if we want to catch this UB in Goblint after the transformation has occurred.
An easy fix would be to enhance goblint-cil to add an attribute to those varinfos that are not encountered at the top scope. Then, we can over-approximate by treating all derefs of such variables as potentially invalid.