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:
old references| Type Params | Return Type | Name and description |
|---|---|---|
|
public void |
visit(ASTNode[] nodes, SourceUnit source)Validates that old references used by @Ensures stay within the state declared by
@Modifies. |
Validates that old references used by @Ensures stay within the state declared by
@Modifies.
nodes - the annotated AST nodes supplied by the compilersource - the current source unit