Support stack-allocating functions when allocating heap vars

[mrstanb]

During the SV-COMP benchmark runs, we noticed that calls to alloca() and __builtin_alloca() result in heap variables being allocated during analysis. However, when passing memory, allocated with these function, to free() no warning was produced, since Goblint couldn't differentiate between stack- and heap-allocated heap vars.

This PR:

• Updates Queries.HeapVar, s.t. it now takes a boolean flag indicating whether the heap variable in the query answer is allocated on the stack or the heap
• Adds Queries.IsDynamicallyAlloced which works like Queries.IsHeapVar with the difference that it also differentiates whether the heap var is one abstracting stack or heap memory

TODOs:

• Track memory, allocated via alloca()-like functions, for each function that calls alloca()-like functions
• Make sure that useAfterFree can free memory, allocated via alloca()-like functions, as soon as a function that called alloca() is returned from

[mrstanb]

I'm only wondering about one thing, namely __builtin_alloca is now defined

• Once as part of c_descs_list
• And once as part of gcc_descs_list

Iirc, __builtin_* functions are GCC-specific and thus it's probably worth it to keep __builtin_alloca only in gcc_descs_list. What do you think?

[sim642]

Indeed there should be just one definition of __builtin_alloca and it should be under GCC. Also alloca itself should go there because it's not part of any C standard. According to the man page, it's not part of any standard, but is "machine- and compiler-dependent".

[mrstanb]

Indeed there should be just one definition of __builtin_alloca and it should be under GCC. Also alloca itself should go there because it's not part of any C standard. According to the man page, it's not part of any standard, but is "machine- and compiler-dependent".

Both alloca and __builtin_alloca should be now part of gcc_descs_list only. Cf. 35513d0

[michael-schwarz]

Sorry for not waiting on your review @sim642, but things are starting to get urgent in order for @mrstanb's changes being all set and integrated with the rest in time for us to still run benchmarks without opening another staging branch and the hassle that creates.
If it turns out later that there's anything that should still be fixed here Stanimir (or I) will address it on master / in a follow-up PR.