org.jmlspecs.jml4.rac
Class JmlNullifier

java.lang.Object
  org.eclipse.jdt.internal.compiler.ASTVisitor
      org.jmlspecs.jml4.rac.DefaultRacAstVisitor
          org.jmlspecs.jml4.rac.JmlNullifier

All Implemented Interfaces:

JavaAstVisitor, JmlAstVisitor, RacAstVisitor

public class JmlNullifier
extends DefaultRacAstVisitor

Constructor Summary

JmlNullifier()

Method Summary

void	endVisit(JmlMethodDeclaration methodDeclaration, ClassScope scope)
void	endVisit(JmlMethodSpecification jmlMethodSpecification, BlockScope scope)
void	endVisit(JmlMethodSpecification jmlMethodSpecification, ClassScope classScope)
void	endVisit(JmlResultReference resultReference, BlockScope scope)
void	endVisit(TypeDeclaration localTypeDeclaration, BlockScope scope)
void	nullify(CompilationUnitDeclaration unit) Retrieves the dirty bits of all the children AST nodes of the given compilation unit and returns them as a new map from AST nodes to their dirty bits.
boolean	visit(JmlMethodDeclaration methodDeclaration, ClassScope scope)
boolean	visit(JmlMethodSpecification jmlMethodSpecification, BlockScope scope)
boolean	visit(JmlMethodSpecification jmlMethodSpecification, ClassScope classScope)
boolean	visit(JmlResultReference resultReference, BlockScope scope) The primary \result can only be used in non-void method.
boolean	visit(TypeDeclaration localTypeDeclaration, BlockScope scope) Declaring an inner type within a method body.

Methods inherited from class org.jmlspecs.jml4.rac.DefaultRacAstVisitor

endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Methods inherited from class org.eclipse.jdt.internal.compiler.ASTVisitor

acceptProblem, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface org.jmlspecs.jml4.rac.JmlAstVisitor

endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Constructor Detail

JmlNullifier

public JmlNullifier()

Method Detail

nullify

public void nullify(CompilationUnitDeclaration unit)

Retrieves the dirty bits of all the children AST nodes of the given compilation unit and returns them as a new map from AST nodes to their dirty bits.

See Also:

AstDirtyBitsRestorer.restore(CompilationUnitDeclaration, Map)

visit

public boolean visit(JmlMethodDeclaration methodDeclaration,
                     ClassScope scope)

Specified by:

visit in interface JmlAstVisitor

Overrides:

visit in class DefaultRacAstVisitor

See Also:

MethodDeclaration

endVisit

public void endVisit(JmlMethodDeclaration methodDeclaration,
                     ClassScope scope)

Specified by:

endVisit in interface JmlAstVisitor

Overrides:

endVisit in class DefaultRacAstVisitor

See Also:

JmlMethodDeclaration

visit

public boolean visit(JmlResultReference resultReference,
                     BlockScope scope)

Description copied from interface: JmlAstVisitor

The primary \result can only be used in non-void method. Its value is the value returned by the method. Its type is the return type of the method. Examples include:

 \result <= x
 \result == x
 

Specified by:

visit in interface JmlAstVisitor

Overrides:

visit in class DefaultRacAstVisitor

endVisit

public void endVisit(JmlResultReference resultReference,
                     BlockScope scope)

Specified by:

endVisit in interface JmlAstVisitor

Overrides:

endVisit in class DefaultRacAstVisitor

See Also:

JmlResultReference

visit

public boolean visit(JmlMethodSpecification jmlMethodSpecification,
                     BlockScope scope)

Specified by:

visit in interface JmlAstVisitor

Overrides:

visit in class ASTVisitor

endVisit

public void endVisit(JmlMethodSpecification jmlMethodSpecification,
                     BlockScope scope)

Specified by:

endVisit in interface JmlAstVisitor

Overrides:

endVisit in class ASTVisitor

visit

public boolean visit(JmlMethodSpecification jmlMethodSpecification,
                     ClassScope classScope)

Specified by:

visit in interface JmlAstVisitor

Overrides:

visit in class DefaultRacAstVisitor

endVisit

public void endVisit(JmlMethodSpecification jmlMethodSpecification,
                     ClassScope classScope)

Specified by:

endVisit in interface JmlAstVisitor

Overrides:

endVisit in class DefaultRacAstVisitor

visit

public boolean visit(TypeDeclaration localTypeDeclaration,
                     BlockScope scope)

Description copied from interface: JavaAstVisitor

Declaring an inner type within a method body. Examples include:

 void m() {
        class A { ... }
 }
 

In this example, class A { ... } is a localTypeDeclaration.

Specified by:

visit in interface JavaAstVisitor

Overrides:

visit in class DefaultRacAstVisitor

endVisit

public void endVisit(TypeDeclaration localTypeDeclaration,
                     BlockScope scope)

Specified by:

endVisit in interface JavaAstVisitor

Overrides:

endVisit in class DefaultRacAstVisitor

See Also:

;