de.uka.ilkd.key.java

Class JavaNonTerminalProgramElement

java.lang.Object

de.uka.ilkd.key.java.JavaSourceElement

de.uka.ilkd.key.java.JavaProgramElement

de.uka.ilkd.key.java.JavaNonTerminalProgramElement

All Implemented Interfaces:

ModelElement, NonTerminalProgramElement, ProgramElement, SourceElement, SVSubstitute

Direct Known Subclasses:

ArrayInitializer, ArrayLengthReference, ArrayReference, BranchImp, CatchAllStatement, CompilationUnit, ExecutionContext, ForUpdates, Guard, Import, InheritanceSpecification, JavaDeclaration, JavaStatement, LoopInit, MetaClassReference, MethodBodyStatement, MethodReference, Operator, PackageReference, PackageSpecification, ProgramTransformer, SpecialConstructorReference, SuperReference, ThisReference, Throws, TypeReferenceImp, VariableReference, VariableSpecification

public abstract class JavaNonTerminalProgramElement
extends JavaProgramElement
implements NonTerminalProgramElement

Top level implementation of a Java NonTerminalProgramElement. taken from COMPOST and changed to achieve an immutable structure

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.java.JavaProgramElement

JavaProgramElement.NameAbstractionTableDisabled

Constructor Summary

Constructors

Constructor and Description
JavaNonTerminalProgramElement()
JavaNonTerminalProgramElement(ExtList list) Java program element.
JavaNonTerminalProgramElement(ExtList children, PositionInfo pos)
JavaNonTerminalProgramElement(PositionInfo pos)

Method Summary

Modifier and Type	Method and Description
protected boolean	compatibleBlockSize(int pos, int max) used by @link matchChildren to decide if a found match is valid or if there are remaining source elements that have not been matched (in which case the match failed)
protected int	computeHashCode()
boolean	equals(java.lang.Object o)
boolean	equalsModRenaming(SourceElement se, NameAbstractionTable nat) commented in interface SourceElement.
protected int	getArrayPos(ImmutableArray<ProgramElement> arr, ProgramElement el) returns the index of element el in array arr
MatchConditions	match(SourceData source, MatchConditions matchCond) matches the source "text" (@link SourceData#getSource()) against the pattern represented by this object.
protected MatchConditions	matchChildren(SourceData source, MatchConditions matchCond, int offset) matches successively all children of this current node.

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

getComments, hashCode, prettyPrint, prettyPrintMain, reuseSignature

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

getEndPosition, getFirstElement, getFirstElementIncludingBlocks, 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.NonTerminalProgramElement

getChildAt, getChildCount

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

getComments

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

getEndPosition, getFirstElement, getFirstElementIncludingBlocks, getLastElement, getPositionInfo, getRelativePosition, getStartPosition, prettyPrint, visit

Constructor Detail

JavaNonTerminalProgramElement

public JavaNonTerminalProgramElement()

JavaNonTerminalProgramElement

public JavaNonTerminalProgramElement(ExtList list)

Java program element.

Parameters:

list - as ExtList with children of the node

JavaNonTerminalProgramElement

public JavaNonTerminalProgramElement(PositionInfo pos)

JavaNonTerminalProgramElement

public JavaNonTerminalProgramElement(ExtList children,
                                     PositionInfo pos)

Method Detail

getArrayPos

protected int getArrayPos(ImmutableArray<ProgramElement> arr,
                          ProgramElement el)

returns the index of element el in array arr

Parameters:

arr - the array where the element is looked for

el - the element to look for

Returns:

the index of the element (-1 if not found)

equalsModRenaming

public boolean equalsModRenaming(SourceElement se,
                                 NameAbstractionTable nat)

commented in interface SourceElement. Overwrites the default method implementation in ProgramElement by descending down to the children.

Specified by:

equalsModRenaming in interface SourceElement

Overrides:

equalsModRenaming in class JavaProgramElement

equals

public boolean equals(java.lang.Object o)

Overrides:

equals in class JavaProgramElement

computeHashCode

protected int computeHashCode()

Overrides:

computeHashCode in class JavaProgramElement

match

public MatchConditions match(SourceData source,
                             MatchConditions matchCond)

Description copied from interface: ProgramElement

matches the source "text" (@link SourceData#getSource()) against the pattern represented by this object. In case of a successful match the resulting MatchConditions with the found instantiations of the schemavariables. If the match failed, null is returned instead.

Specified by:

match in interface ProgramElement

Overrides:

match in class JavaProgramElement

Parameters:

source - the SourceData with the program element to match

matchCond - the MatchConditions found up to this point

Returns:

the resulting match conditions or null if the match failed

compatibleBlockSize

protected boolean compatibleBlockSize(int pos,
                                      int max)

used by @link matchChildren to decide if a found match is valid or if there are remaining source elements that have not been matched (in which case the match failed)

matchChildren

protected MatchConditions matchChildren(SourceData source,
                                        MatchConditions matchCond,
                                        int offset)

matches successively all children of this current node. Thereby the offset-th child is matched against source.getSource(). The call source.next has to be done in the @link ProgramElement#match method of the currently matched child in case of a successful match. This is not done here (rationale: schemavariables matching on lists can be implemented easy).

Parameters:

source - the SourceData with the children to be matched

matchCond - the MatchConditions found so far

offset - the int denoting the index of the child to start with

Returns:

the resulting match conditions or null if matching failed