Implement a new XlangAnalysisPhase

This commit introduces a new XlangAnalysisPhase that run
all the xlang phase as well as the AnalysisPhase. It updates
the Main accordingly.

The reason for this change is to be able to correctly control
the --functions option as well as transforming each VerificationCondition
about function postcondition into loop invariant.

The previous solution was to use some mutable states inside the FunDef object.
Those are cleaned by this commit. To do so, it was necessary to change the
transformation phases signature in order to return along with the modified
program a Set or Map (depending on which phase) of freshly introduced
functions and their correspondance in the original program.

One small change that was necessary was to not print the verification report
in the analysis phase but only in the Main. This allows the XlangAnalysisPhase
to update correctly the verification conditions in the report before it gets
printed. This is also arguably a better design decision to have it printed
in the Main since it was returned by the AnalysisPhase.