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

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

more compact assign clauses for state variables, and remove useless memory pack predicates and assertions

more agressive optim propagation in spec in order to remove unecessarry existential variables that were eliminated (helps the solvers)

the generation of ACSL from machine code reveal too fragile as it occurs after several transformations (eg. fusion)

- real constants are hidden in Real.ml{i} module

  use the same polymorphic type in variables and values.

- now properly records the scopes
- only register requested ones