org.jmlspecs.jml4.rac
Class InlineAssertionVisitor

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

public class InlineAssertionVisitor
extends ASTVisitor

Visitor class to translate a JML in-line assertion into RAC code.

Developer's note: The node of translated RAC code is later merged to the node of its in-line assertion during the AST merging phase. For this, this class works in a close collaboration with the InlineAssertionMerger. Thus, when a new JML in-line assertion is supported for RAC, both classes should be reviewed; in particular, the @{link isRacInlineAssertion(Statement)} should be revised to include the newly supported in-line assertion; this method is used by the merger class. In general, it requires two steps:

1. Add a visitor method to translate the new in-line assertion.
2. Modify the isRacInlineAssertion(Statement) method to state that the new in-line assertion is RAC-compiled.

Author:

Amritam Sarcar and Yoonsik Cheon

Constructor Summary

InlineAssertionVisitor()
Creates a new translator.

Method Summary

void	checkJmlStatement(JmlSetStatement stmt)
void	endVisit(Block block, BlockScope scope) Overridden Visitor methods to keep track of inline statements that are not embedded inside blocks.
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 jmlforeachStatement, BlockScope scope)
void	endVisit(JmlForStatement forStatement, BlockScope scope)
void	endVisit(JmlWhileStatement jmlwhileStatement, BlockScope scope)
void	endVisit(LabeledStatement labeledStatement, BlockScope scope)
void	endVisit(WhileStatement whileStatement, BlockScope scope)
static boolean	isLoopAnnotated(Statement stmt)
static boolean	isRacInlineAssertion(Statement stmt) Return true if the given statement is a JML in-line assertion and currently supported for RAC.
java.lang.StringBuffer	translate(AbstractMethodDeclaration meth, RacResult result) Translates all in-line assertions contained in the body of the given method to RAC code in the AST visitor traversal order and return the translated RAC code.
java.lang.StringBuffer	translate(Initializer initBlock, RacResult result) Translates all jml-assertion statements in Initializer blocks.
java.lang.StringBuffer	translate(Statement stmt, AbstractMethodDeclaration meth, RacResult result) Translates the given (in-line assertion) statement in the context of the given method and returns the translated RAC code.
boolean	visit(Block block, BlockScope scope)
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(JmlAssertStatement stmt, BlockScope scope) Overridden here to visit and translate the given JML assert statement into RAC code.
boolean	visit(JmlAssumeStatement stmt, BlockScope scope) Overridden here to visit and translate the given JML assume statement into RAC code.
boolean	visit(JmlDoStatement doStatement, BlockScope scope)
boolean	visit(JmlForeachStatement foeachStatement, BlockScope scope)
boolean	visit(JmlForStatement forStatement, BlockScope scope)
boolean	visit(JmlSetStatement stmt, BlockScope scope) Overridden here to visit and translate the given JML set statement into RAC code.
boolean	visit(JmlWhileStatement whileStatement, 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, 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

Methods inherited from class java.lang.Object

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

Constructor Detail

InlineAssertionVisitor

public InlineAssertionVisitor()

Creates a new translator.

Method Detail

translate

public java.lang.StringBuffer translate(AbstractMethodDeclaration meth,
                                        RacResult result)

Translates all in-line assertions contained in the body of the given method to RAC code in the AST visitor traversal order and return the translated RAC code. The resulting RAC code is a sequence of statements, one for each in-line assertion. Other translation information is stored in result.

translate

public java.lang.StringBuffer translate(Initializer initBlock,
                                        RacResult result)

Translates all jml-assertion statements in Initializer blocks.

See Also:

translateMethod

isRacInlineAssertion

public static boolean isRacInlineAssertion(Statement stmt)

Return true if the given statement is a JML in-line assertion and currently supported for RAC.

This method is used by InlineAssertionMerger to merge the translated RAC code to its original in-line assertion. Thus, it has to be revised whenever a new JML in-line assertion becomes supported for RAC.

translate

public java.lang.StringBuffer translate(Statement stmt,
                                        AbstractMethodDeclaration meth,
                                        RacResult result)

Translates the given (in-line assertion) statement in the context of the given method and returns the translated RAC code.

visit

public boolean visit(JmlAssertStatement stmt,
                     BlockScope scope)

Overridden here to visit and translate the given JML assert statement into RAC code.

Overrides:

visit in class ASTVisitor

visit

public boolean visit(JmlAssumeStatement stmt,
                     BlockScope scope)

Overridden here to visit and translate the given JML assume statement into RAC code.

Overrides:

visit in class ASTVisitor

visit

public boolean visit(JmlSetStatement stmt,
                     BlockScope scope)

Overridden here to visit and translate the given JML set statement into RAC code.

Overrides:

visit in class ASTVisitor

checkJmlStatement

public void checkJmlStatement(JmlSetStatement stmt)

visit

public boolean visit(JmlWhileStatement whileStatement,
                     BlockScope scope)

Overrides:

visit in class ASTVisitor

visit

public boolean visit(JmlDoStatement doStatement,
                     BlockScope scope)

Overrides:

visit in class ASTVisitor

visit

public boolean visit(JmlForStatement forStatement,
                     BlockScope scope)

Overrides:

visit in class ASTVisitor

visit

public boolean visit(JmlForeachStatement foeachStatement,
                     BlockScope scope)

Overrides:

visit in class ASTVisitor

isLoopAnnotated

public static boolean isLoopAnnotated(Statement stmt)

endVisit

public void endVisit(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:

endVisit in class ASTVisitor

visit

public boolean visit(Block block,
                     BlockScope scope)

Overrides:

visit in class ASTVisitor

endVisit

public void endVisit(JmlWhileStatement jmlwhileStatement,
                     BlockScope scope)

Overrides:

endVisit in class ASTVisitor

endVisit

public void endVisit(JmlForeachStatement jmlforeachStatement,
                     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

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

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