de.uka.ilkd.key.java.reference

Class SuperConstructorReference

java.lang.Object

de.uka.ilkd.key.java.JavaSourceElement

de.uka.ilkd.key.java.JavaProgramElement

de.uka.ilkd.key.java.JavaNonTerminalProgramElement

de.uka.ilkd.key.java.reference.SpecialConstructorReference

de.uka.ilkd.key.java.reference.SuperConstructorReference

All Implemented Interfaces:

ExpressionContainer, ModelElement, NonTerminalProgramElement, ProgramElement, Reference, ConstructorReference, MemberReference, MethodOrConstructorReference, ReferencePrefix, ReferenceSuffix, SourceElement, Statement, SVSubstitute

public class SuperConstructorReference
extends SpecialConstructorReference
implements ReferenceSuffix

Super constructor reference.

Field Summary

Fields

Modifier and Type	Field and Description
protected ReferencePrefix	prefix Access path to enclosing class.

Fields inherited from class de.uka.ilkd.key.java.reference.SpecialConstructorReference

arguments

Constructor Summary

Constructors

Constructor and Description
SuperConstructorReference()
SuperConstructorReference(Expression[] arguments) Super constructor reference.
SuperConstructorReference(ExtList children, ReferencePrefix accessPath) Constructor for the transformation of COMPOST ASTs to KeY.
SuperConstructorReference(ExtList children, ReferencePrefix accessPath, PositionInfo pi) Constructor for the transformation of COMPOST ASTs to KeY.
SuperConstructorReference(ReferencePrefix accessPath, Expression[] arguments) Super constructor reference.
SuperConstructorReference(ReferencePrefix accessPath, ImmutableArray<Expression> arguments) Super constructor reference.

Method Summary

Modifier and Type	Method and Description
SourceElement	getFirstElement() Finds the source element that occurs first in the source.
SourceElement	getFirstElementIncludingBlocks() Finds the source element that occurs first in the source.
ReferencePrefix	getReferencePrefix()
void	prettyPrint(PrettyPrinter p) Pretty printing the source element.
void	visit(Visitor v) calls the corresponding method of a visitor in order to perform some action/transformation on this element

Methods inherited from class de.uka.ilkd.key.java.reference.SpecialConstructorReference

getArguments, getChildAt, getChildCount, getExpressionAt, getExpressionCount

Methods inherited from class de.uka.ilkd.key.java.JavaNonTerminalProgramElement

compatibleBlockSize, computeHashCode, equals, equalsModRenaming, getArrayPos, match, matchChildren

Methods inherited from class de.uka.ilkd.key.java.JavaProgramElement

getComments, hashCode, prettyPrintMain, reuseSignature

Methods inherited from class de.uka.ilkd.key.java.JavaSourceElement

getEndPosition, getLastElement, getParentClass, getPositionInfo, getRelativePosition, getStartPosition, setParentClass, toSource, toString, toString

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.java.ProgramElement

getComments, match

Methods inherited from interface de.uka.ilkd.key.java.SourceElement

equalsModRenaming, getEndPosition, getLastElement, getPositionInfo, getRelativePosition, getStartPosition

Field Detail

prefix

protected final ReferencePrefix prefix

Access path to enclosing class. As KeY normalises inner classes this should be always null and may be removed in future

Constructor Detail

SuperConstructorReference

public SuperConstructorReference()

SuperConstructorReference

public SuperConstructorReference(Expression[] arguments)

Super constructor reference.

Parameters:

arguments - an expression mutable list.

SuperConstructorReference

public SuperConstructorReference(ReferencePrefix accessPath,
                                 Expression[] arguments)

Super constructor reference.

Parameters:

accessPath - a reference prefix.

arguments - an expression mutable list.

SuperConstructorReference

public SuperConstructorReference(ReferencePrefix accessPath,
                                 ImmutableArray<Expression> arguments)

Super constructor reference.

Parameters:

accessPath - a reference prefix.

arguments - an expression mutable list.

SuperConstructorReference

public SuperConstructorReference(ExtList children,
                                 ReferencePrefix accessPath,
                                 PositionInfo pi)

Constructor for the transformation of COMPOST ASTs to KeY.

Parameters:

children - the children of this AST element as KeY classes.

accessPath - a ReferencePrefix of the array reference. May contain: several of Expression (as initializers of the array), Comments. Must contain: execution context MUST NOT CONTAIN: the ReferencePrefix for the accessPath because Expression and ReferencePrefix might not be disjunct.

SuperConstructorReference

public SuperConstructorReference(ExtList children,
                                 ReferencePrefix accessPath)

Constructor for the transformation of COMPOST ASTs to KeY.

Parameters:

children - the children of this AST element as KeY classes.

accessPath - a ReferencePrefix of the array reference. May contain: several of Expression (as initializers of the array), Comments. Must contain: execution context MUST NOT CONTAIN: the ReferencePrefix for the accessPath because Expression and ReferencePrefix might not be disjunct.

Method Detail

getReferencePrefix

public ReferencePrefix getReferencePrefix()

Specified by:

getReferencePrefix in interface ReferencePrefix

getFirstElement

public SourceElement getFirstElement()

Description copied from class: JavaSourceElement

Finds the source element that occurs first in the source. The default implementation returns this element, which is correct for all terminal program elements, and many non terminals such as statements and prefixed operators.

Specified by:

getFirstElement in interface SourceElement

Overrides:

getFirstElement in class JavaSourceElement

Returns:

the first source element in the syntactical representation of this element, may be equals to this element.

See Also:

JavaSourceElement.toSource(), JavaSourceElement.getStartPosition()

getFirstElementIncludingBlocks

public SourceElement getFirstElementIncludingBlocks()

Description copied from interface: SourceElement

Finds the source element that occurs first in the source.

Specified by:

getFirstElementIncludingBlocks in interface SourceElement

Overrides:

getFirstElementIncludingBlocks in class JavaSourceElement

Returns:

the first source element in the syntactical representation of this element, may be equals to this element.

See Also:

SourceElement.getStartPosition()

visit

public void visit(Visitor v)

Description copied from interface: SourceElement

calls the corresponding method of a visitor in order to perform some action/transformation on this element

Specified by:

visit in interface SourceElement

Parameters:

v - the Visitor

prettyPrint

public void prettyPrint(PrettyPrinter p)
                 throws java.io.IOException

Description copied from class: JavaSourceElement

Pretty printing the source element.

Specified by:

prettyPrint in interface SourceElement

Overrides:

prettyPrint in class JavaProgramElement

Parameters:

p - a pretty printer.

Throws:

java.io.IOException - occasionally thrown.