Instead, emits an error but continues the analysis with the probably unsound
specification generated by the kernel.
Also prints the callstack when -eva-print-callstacks is enabled.

Cherry-picked from stable/nupw

Catches the exception [SizeOfError] when using [Cil.bytesAlignOf].

On recursive calls, the substitution to be applied to the domain states is not
applied to the valuation given as argument to [start_call].
This commit:
- adds comment in the abstract domain signature to reflect this fact;
- fixes the domains to properly use the valuation in recursive calls.

The equality and octagon domains are now intra-procedural on recursive calls:
they always start the analysis of a recursive call with an empty state.

Instead of the deprecated parameter -eva-ignore-recursive-calls.

Applies the substitution of local and formal variables to the  copy of variables
in recursive calls.

Instead of the deprecated parameter -eva-ignore-recursive-calls.