Mentions légales du service

Skip to content

Unused variables message

DAILLER Sylvain requested to merge issue_346 into master

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
Edited by MARCHE Claude

Merge request reports