Unused variables message
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