Handling of CIL variable renaming for witness invariant generation and parsing

[sim642]

Problem pointed out here: #745 (comment).

Good point, I didn't think about it here, but I think there's not much to do about it either. On the witness generation side, there's InvariantCil.exp_replace_original_name that maps things to original names. But here for parsing we'd somehow need to know, which of the variables with the same original name was in scope at a particular location inside the function after they've been all pulled up and renamed.

As I mentioned in goblint/cil#97, the normal Cabs2cil uses tons of global variables to keep track of things and these block scopes and alpha renaming tables (and undos in alpha renaming tables) are among those. But all those structures are mutated, so we cannot go back to a particular location and have the exact state of those internal globals that normally keep track of this. One way would be to keep the CABS of all functions around and redo Cabs2cil for the function where the invariant belongs to, so it reconstructs that state, such that we can convert the invariant expression exactly as it would have been at a particular location and abort Cabs2cil, but that seems super ugly.

But here's a maybe radical idea: we make CIL not do those renames at all and just continue with a single fundec containing multiple local varinfos with same vname. Since we identify variables by vid, not vname, this should have no effect on the semantics, only results presentation (which is nicer with less renaming anyway). And somehow also eliminate the pulling up of all locals from all block scopes, such that the scopes are also later observable.

Anyway, tackling that whole issue is probably too much to do right here, but for the time being, a variable name in the expression would just find the first varinfo that has it unrenamed. All the others would have names with suffixes, which won't be used unless you directly also use that name in the invariant, but that would violate the semantics of it being insertable as an assertion.