-
Adam Nelson authored
The current version of the Mu specification does not use $-variables to pass return values from terminsts to the normal destination of an EXC clause, instead allowing terminsts to have normal SSA return values that may be referenced in the EXC clause. This commit updates the formalism to match. Several other refactorings are included, such as making exec_terminst only return modified stacks, using a simpler representation of common instructions, and defining prefix/infix operators for SSA variables and registers in HOL.
d4b31059