Dynamic local struct allocation

[s0mark]

Makes local variable struct address allocation happen dynamically during verification, as opposed to statically in the frontend phase. Fixes #474.

The key challenge to overcome here is to figure out whether or not a local variable is a compound type when a procedure is called. From my understanding, this information is only tracked in the frontend and cannot be retrieved from a VarDecl or its .ref expression without some parseContext.

This solution adds optional initializers to all local variables of an XcfaProcedure, which can be called to generate an initializing expression. When a procedure call is encountered, the generated expression is assigned to the new instance of the local variable, at the same time when parameters are assigned. The initializers are added in the frontend phase and are only used for this purpose at this point.

Another approach I considered was to collect such local variables in a procedure pass and store them in a some heap class, along with their CComplexType (for the address type). Upon a procedure call, this collection could be queried to retrieve the initializing memory address for a local variable, if required. I decided on the former solution, as it seemed more cohesive.

If there's a preferred, perhaps less intrusive way of retrieving the necessary information, please let me know!

[leventeBajczi]

I'm afraid this breaks non-CEGAR approaches -- even though they would fail anyway due to dereference not being translated, that can/will be fixed at some point, and we'll get silent failures/wrong results for non-initialized struct variables.

The original problem is, as far as I understand it, that we used a fix pointer base value for the local struct. Then, in a recursive call, we did not properly 'reallocate' it, but kept using the same base value.

The trivial solution to me would be to get rid of stack-allocation here (it is unsound, after all) and divert it to the same machinery as what handles malloc() and co. What do you think?