The semantics of external function calls in LTL, Linear, Mach and Asm
now consider that all caller-save registers are set to Vundef by the call.
This models that fact that the external function can modify those registers
arbitrarily.

Update the proofs of the Allocation, Tunneling, Stacking and Asmgen passes
accordingly.