Move extern inits, global inits and otherfuns spawning into constraint system

[sim642]

Currently extern inits, global inits and otherfuns spawning is done by manually simulating transfer function calls with degenerate ctx: https://github.com/goblint/analyzer/blob/20f3a7d6285a35c7c7d5c2f6206e280a73b83c25/src/framework/control.ml#L175-L349

In my experience, time and time again, this has been causing issues because: 1.ctxs are degenerate – some outright crash, others have behavior which doesn't match the one available during solving;

2. it somewhat duplicates what FromSpec does;
3. it misses some nontrivial things that would happen during actual solving – e.g. main is unaware of otherfuns having been spawned at all;
4. it's extremely error prone and hard to maintain.

The sensible thing would be to do all these things within the constraint system and let the solver evaluate them.

[sim642]

Turns out there is yet another maniacal form of global initialization that we handle in yet another weird way: by adding them as calls into the main function to be performed during the solving, not during our global inits. No idea if any sane person uses them, since we have some support, their handling should also be made uniform with the rest.

https://github.com/goblint/analyzer/blob/c398773746841ff7e51525f4911c831368b626ce/src/util/cilfacade.ml#L136-L149

https://github.com/goblint/analyzer/blob/c398773746841ff7e51525f4911c831368b626ce/src/util/cilfacade.ml#L109-L121

[vogler]

Are these C++ class constructors or some other feature in C?

[sim642]

It's a C thing. From GCC manual:

The constructor attribute causes the function to be called automatically before execution enters main (). [...] Functions with these attributes are useful for initializing data that is used implicitly during the execution of the program.