Description:
- Choice was made to not add unused variables when there is no contract
and no body (no pre/(x)post, and no body).
- For postcondition variable result, we only check variables that are not
of unit type. And, we report a warning only if the variable is not present
in all the ensures.
- For result variable, with several imbricated raise, it seems possible to
have false positive with no location. Removing the no location case which
seems unhelpful anyway
The warning can be disabled by a debug flag.
The bench was changed so as to accept examples that **should** output
warning but not fail (this category did not exist, it does now) and
label_scope has been switched to it.
