org.jmlspecs.jml4.rac
Class InlineAssertionMerger

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

public class InlineAssertionMerger
extends ASTVisitor

Merges RAC code of JML in-line assertions to their original assertions.

Author:

Amritam Sarcar and Yoonsik Cheon

See Also:

merge(Statement[], Statement[])

Constructor Summary

InlineAssertionMerger()
Creates a new merger.

Method Summary

void	endVisit(Block block, BlockScope scope) Overridden here to replace JML in-line assertions contained in the given block with their RAC code.
void	endVisit(DoStatement doStatement, BlockScope scope)
void	endVisit(ForeachStatement forStatement, BlockScope scope)
void	endVisit(ForStatement forStatement, BlockScope scope)
void	endVisit(IfStatement ifStatement, BlockScope scope)
void	endVisit(JmlDoStatement doStatement, BlockScope scope)
void	endVisit(JmlForeachStatement foreachStatement, BlockScope scope)
void	endVisit(JmlForStatement forStatement, BlockScope scope)
void	endVisit(JmlWhileStatement jmlwhileStatement, BlockScope scope)
void	endVisit(LabeledStatement labeledStatement, BlockScope scope)
void	endVisit(LocalDeclaration localDeclaration, BlockScope scope) A visitor method to check whether a localDeclaration have ghost modifier, ghost.
void	endVisit(WhileStatement whileStatement, BlockScope scope)
void	merge(Statement[] to, Statement[] from) Merges RAC code of JML in-line assertions contained in from to the ASTs of to.
boolean	visit(Block block, BlockScope scope) Overridden Visitor methods to keep track of inline statements that are not embedded inside blocks.
boolean	visit(DoStatement doStatement, BlockScope scope)
boolean	visit(ForeachStatement forStatement, BlockScope scope)
boolean	visit(ForStatement forStatement, BlockScope scope)
boolean	visit(IfStatement ifStatement, BlockScope scope)
boolean	visit(LabeledStatement labeledStatement, BlockScope scope)
boolean	visit(WhileStatement whileStatement, BlockScope scope)

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, 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, 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

Constructor Detail

InlineAssertionMerger

public InlineAssertionMerger()

Creates a new merger.

Method Detail

merge

public void merge(Statement[] to,
                  Statement[] from)

Merges RAC code of JML in-line assertions contained in from to the ASTs of to. This method replaces every JML in-line assertion in to, directly or indirectly (as a nested statement), with its RAC code located in from. If to[i] (or its child node) is a JML in-line assertion, its RAC code is found in from[j], where j is the index given in terms of the AST visitor traversal order.

  requires to != null && from != null;
 

endVisit

public void endVisit(Block block,
                     BlockScope scope)

Overridden here to replace JML in-line assertions contained in the given block with their RAC code.

Overrides:

endVisit in class ASTVisitor

endVisit

public void endVisit(LocalDeclaration localDeclaration,
                     BlockScope scope)

A visitor method to check whether a localDeclaration have ghost modifier, ghost. If it contains, it is commented, in this case it is removed.

Overrides:

endVisit in class ASTVisitor

visit

public boolean visit(Block block,
                     BlockScope scope)

Overridden Visitor methods to keep track of inline statements that are not embedded inside blocks.

 if (C)
                
 

Such examples can be associated with if, if-else, if-elseif, while, for, do-while statements.

Overrides:

visit in class ASTVisitor

endVisit

public void endVisit(JmlWhileStatement jmlwhileStatement,
                     BlockScope scope)

Overrides:

endVisit in class ASTVisitor

endVisit

public void endVisit(JmlDoStatement doStatement,
                     BlockScope scope)

Overrides:

endVisit in class ASTVisitor

endVisit

public void endVisit(JmlForStatement forStatement,
                     BlockScope scope)

Overrides:

endVisit in class ASTVisitor

endVisit

public void endVisit(JmlForeachStatement foreachStatement,
                     BlockScope scope)

Overrides:

endVisit in class ASTVisitor

visit

public boolean visit(LabeledStatement labeledStatement,
                     BlockScope scope)

Overrides:

visit in class ASTVisitor

endVisit

public void endVisit(LabeledStatement labeledStatement,
                     BlockScope scope)

Overrides:

endVisit in class ASTVisitor

visit

public boolean visit(DoStatement doStatement,
                     BlockScope scope)

Overrides:

visit in class ASTVisitor

endVisit

public void endVisit(DoStatement doStatement,
                     BlockScope scope)

Overrides:

endVisit in class ASTVisitor

visit

public boolean visit(ForeachStatement forStatement,
                     BlockScope scope)

Overrides:

visit in class ASTVisitor

endVisit

public void endVisit(ForeachStatement forStatement,
                     BlockScope scope)

Overrides:

endVisit in class ASTVisitor

visit

public boolean visit(ForStatement forStatement,
                     BlockScope scope)

Overrides:

visit in class ASTVisitor

endVisit

public void endVisit(ForStatement forStatement,
                     BlockScope scope)

Overrides:

endVisit in class ASTVisitor

visit

public boolean visit(IfStatement ifStatement,
                     BlockScope scope)

Overrides:

visit in class ASTVisitor

endVisit

public void endVisit(IfStatement ifStatement,
                     BlockScope scope)

Overrides:

endVisit in class ASTVisitor

visit

public boolean visit(WhileStatement whileStatement,
                     BlockScope scope)

Overrides:

visit in class ASTVisitor

endVisit

public void endVisit(WhileStatement whileStatement,
                     BlockScope scope)

Overrides:

endVisit in class ASTVisitor