All Implemented Interfaces and Traits:

ASTTransformation

public class ModifiesEnsuresValidationTransformation
extends Object
implements ASTTransformation

Validates that @Ensures postconditions on a method only reference fields via old.xxx that are declared as modifiable by @Modifies.

Runs at CompilePhase.INSTRUCTION_SELECTION after both:

• ModifiesASTTransformation has stored the modification set, and
• AnnotationClosureVisitor has recorded the old references

Since:

6.0.0

See Also:

Modifies