formatting

add an exhaustivity parameter to Branch constructor in Machine Code to handle C switch default case optimization in case of a singleton enum

ast modifs and additional arrow_taint phase to retrieve which arrow "protects" / "taints" which variable

since the df optim backward optim has been disabled, elimination is in a fixpoint now so elim chains are taken into account

use ghost variables instead of existential variables to avoid read / write capture problems with variable reuse

Discussion w Xavier: replace this mechanism (fragile because of non-constructive witnesses) with a ghost-variables-based mechanism