de.uka.ilkd.key.java.recoderext

Class RMethodBodyStatement

java.lang.Object

recoder.java.JavaSourceElement

recoder.java.JavaProgramElement

recoder.java.JavaNonTerminalProgramElement

recoder.java.statement.JavaStatement

de.uka.ilkd.key.java.recoderext.RMethodBodyStatement

All Implemented Interfaces:

KeYRecoderExtension, java.io.Serializable, java.lang.Cloneable, ExpressionContainer, NamedProgramElement, NonTerminalProgramElement, ProgramElement, TypeReferenceContainer, SourceElement, Statement, ModelElement, NamedModelElement

public class RMethodBodyStatement
extends JavaStatement
implements KeYRecoderExtension, TypeReferenceContainer, ExpressionContainer, NamedProgramElement

See Also:

Serialized Form

Nested Class Summary

Nested classes/interfaces inherited from interface recoder.NamedModelElement

NamedModelElement.LexicalOrder

Nested classes/interfaces inherited from interface recoder.java.ProgramElement

ProgramElement.TreeStructure

Nested classes/interfaces inherited from interface recoder.java.SourceElement

SourceElement.Position

Field Summary

Fields

Modifier and Type	Field and Description
private ASTList<Expression>	arguments
private TypeReference	bodySource
private Identifier	methodName
private ReferencePrefix	methodReferencePrefix
private ProgramVariableSVWrapper	resultVar
private static long	serialVersionUID

Fields inherited from class recoder.java.statement.JavaStatement

parent

Fields inherited from class recoder.java.JavaProgramElement

comments

Fields inherited from class recoder.java.JavaSourceElement

factory

Fields inherited from interface recoder.NamedModelElement

LEXICAL_ORDER

Fields inherited from interface recoder.java.ProgramElement

STRUCTURAL_EQUALITY, STRUCTURAL_HASH_CODE

Constructor Summary

Constructors

Constructor and Description
RMethodBodyStatement(TypeReference typeRef, ProgramVariableSVWrapper resVar, MethodReference mr)
RMethodBodyStatement(TypeReference typeRef, ProgramVariableSVWrapper resVar, ReferencePrefix prefix, Identifier methodName, ASTList<Expression> arguments)

Method Summary

Modifier and Type	Method and Description
void	accept(SourceVisitor visitor)
RMethodBodyStatement	deepClone()
TypeReference	getBodySource()
ProgramElement	getChildAt(int index) Returns the child at the specified index in this node's "virtual" child array
int	getChildCount() Returns the number of children of this node.
int	getChildPositionCode(ProgramElement child)
Expression	getExpressionAt(int index)
int	getExpressionCount()
Identifier	getIdentifier()
MethodReference	getMethodReference()
java.lang.String	getName()
ProgramVariableSVWrapper	getResultVar()
TypeReference	getTypeReferenceAt(int index)
int	getTypeReferenceCount()
void	makeParentRoleValid() Ensures that each child has "this" as syntactical parent.
boolean	replaceChild(ProgramElement p, ProgramElement q) Replace a single child in the current node.
void	setIdentifier(Identifier methodName)
void	setMethodReference(MethodReference methRef) Set the MethodReference that caused this call.

Methods inherited from class recoder.java.statement.JavaStatement

getASTParent, getStatementContainer, setStatementContainer

Methods inherited from class recoder.java.JavaNonTerminalProgramElement

getIndexOfChild, getIndexOfChild, getRoleOfChild, makeAllParentRolesValid, validateAll

Methods inherited from class recoder.java.JavaProgramElement

getComments, setComments, validate

Methods inherited from class recoder.java.JavaSourceElement

getEndPosition, getFactory, getFirstElement, getLastElement, getRelativePosition, getStartPosition, setEndPosition, setRelativePosition, setStartPosition, toSource

Methods inherited from class java.lang.Object

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

Methods inherited from interface recoder.java.NonTerminalProgramElement

getIndexOfChild, getIndexOfChild, getRoleOfChild, makeAllParentRolesValid, validateAll

Methods inherited from interface recoder.java.ProgramElement

getASTParent, getComments, setComments

Methods inherited from interface recoder.java.SourceElement

getEndPosition, getFactory, getFirstElement, getLastElement, getRelativePosition, getStartPosition, setEndPosition, setRelativePosition, setStartPosition, toSource

Field Detail

serialVersionUID

private static final long serialVersionUID

See Also:

Constant Field Values

bodySource

private TypeReference bodySource

resultVar

private ProgramVariableSVWrapper resultVar

methodReferencePrefix

private ReferencePrefix methodReferencePrefix

methodName

private Identifier methodName

arguments

private ASTList<Expression> arguments

Constructor Detail

RMethodBodyStatement

public RMethodBodyStatement(TypeReference typeRef,
                            ProgramVariableSVWrapper resVar,
                            MethodReference mr)

RMethodBodyStatement

public RMethodBodyStatement(TypeReference typeRef,
                            ProgramVariableSVWrapper resVar,
                            ReferencePrefix prefix,
                            Identifier methodName,
                            ASTList<Expression> arguments)

Method Detail

accept

public void accept(SourceVisitor visitor)

Specified by:

accept in interface SourceElement

deepClone

public RMethodBodyStatement deepClone()

Specified by:

deepClone in interface SourceElement

Specified by:

deepClone in interface Statement

setMethodReference

public void setMethodReference(MethodReference methRef)

Set the MethodReference that caused this call.

getChildCount

public int getChildCount()

Returns the number of children of this node.

Specified by:

getChildCount in interface NonTerminalProgramElement

Returns:

an int giving the number of children of this node

getChildAt

public ProgramElement getChildAt(int index)

Returns the child at the specified index in this node's "virtual" child array

Specified by:

getChildAt in interface NonTerminalProgramElement

Parameters:

index - an index into this node's "virtual" child array

Returns:

the program element at the given position

Throws:

java.lang.ArrayIndexOutOfBoundsException - if index is out of bounds

getChildPositionCode

public int getChildPositionCode(ProgramElement child)

Specified by:

getChildPositionCode in interface NonTerminalProgramElement

makeParentRoleValid

public void makeParentRoleValid()

Ensures that each child has "this" as syntactical parent.

Specified by:

makeParentRoleValid in interface NonTerminalProgramElement

Overrides:

makeParentRoleValid in class JavaNonTerminalProgramElement

replaceChild

public boolean replaceChild(ProgramElement p,
                            ProgramElement q)

Replace a single child in the current node. The child to replace is matched by identity and hence must be known exactly. The replacement element can be null - in that case, the child is effectively removed. The parent role of the new child is validated, while the parent link of the replaced child is left untouched.

Specified by:

replaceChild in interface NonTerminalProgramElement

Parameters:

p - the old child.

q - the new child.

Returns:

true if a replacement has occured, false otherwise.

Throws:

java.lang.ClassCastException - if the new child cannot take over the role of the old one.

getBodySource

public TypeReference getBodySource()

getResultVar

public ProgramVariableSVWrapper getResultVar()

getMethodReference

public MethodReference getMethodReference()

getTypeReferenceCount

public int getTypeReferenceCount()

Specified by:

getTypeReferenceCount in interface TypeReferenceContainer

getTypeReferenceAt

public TypeReference getTypeReferenceAt(int index)

Specified by:

getTypeReferenceAt in interface TypeReferenceContainer

getExpressionCount

public int getExpressionCount()

Specified by:

getExpressionCount in interface ExpressionContainer

getExpressionAt

public Expression getExpressionAt(int index)

Specified by:

getExpressionAt in interface ExpressionContainer

getIdentifier

public Identifier getIdentifier()

Specified by:

getIdentifier in interface NamedProgramElement

setIdentifier

public void setIdentifier(Identifier methodName)

Specified by:

setIdentifier in interface NamedProgramElement

getName

public java.lang.String getName()

Specified by:

getName in interface NamedModelElement