| java.lang.Object
 de.uka.ilkd.key.rule.soundness.ProgramSVSkolem
All known Subclasses: de.uka.ilkd.key.rule.soundness.ProgramSVSkolemStatement, de.uka.ilkd.key.rule.soundness.ProgramSVSkolemExpression,
| ProgramSVSkolem | | abstract public class ProgramSVSkolem implements StateDependingObject,NonTerminalProgramElement(Code) | | This class represents statement and expression skolem symbols, which can be
used within programs. Instances of (the subclasses of) this class can be
used as operator together with the class ProgramSVProxy
|
| ProgramSVSkolem | | public ProgramSVSkolem(ProgramElementName p_name, ArrayOfKeYJavaType p_influencingPVTypes, int p_jumpCnt)(Code) | |
Parameters:
p_name - The name of the symbol
Parameters:
p_influencingPVTypes - An array of the types of the program variablearguments
Parameters:
p_jumpCnt - the size of the jump table |
| checkInfluencingPVs | | public boolean checkInfluencingPVs(ArrayOfIProgramVariable p_influencingPVs)(Code) | | |
| checkJumpTable | | public boolean checkJumpTable(ArrayOfStatement p_jumpTable)(Code) | | |
| equalsModRenaming | | public boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat)(Code) | | This method returns true if two program parts are equal modulo
renaming. The equality is mainly a syntactical equality with
some exceptions: if a variable is declared we abstract from the
name of the variable, so the first declared variable gets
e.g. the name decl_1, the second declared decl_2 and so on.
Look at the following programs:
{int i; i=0;} and { int j; j=0;} these would be seen like
{int decl_1; decl_1=0;} and {int decl_1; decl_1=0;} which are
syntactical equal and therefore true is returned (same thing for
labels). But {int i; i=0;} and {int j; i=0;} (in the second
block the variable i is declared somewhere outside)
would be seen as {int decl_1; decl_1=0;} for the first one but
{int decl_1; i=0;} for the second one. These are not
syntactical equal, therefore false is returned.
|
| getAnnotationCount | | public int getAnnotationCount()(Code) | | |
| getChildAt | | public ProgramElement getChildAt(int index)(Code) | | Returns the child at the specified index in this node's "virtual"
child array.
Parameters:
index - an index into this node's "virtual" child array the program element at the given position
exception:
ArrayIndexOutOfBoundsException - if index is outof bounds |
| getChildCount | | public int getChildCount()(Code) | | Returns the number of children of this node.
an int giving the number of children of this node |
| getComments | | public Comment[] getComments()(Code) | | Get comments.
the comments. |
| getEndPosition | | public Position getEndPosition()(Code) | | Returns the end position of the primary token of this element.
To get the end position of the syntactical first token,
call the corresponding method of getLastElement().
the end position of the primary token. |
| getInfluencingPVTypes | | public ArrayOfKeYJavaType getInfluencingPVTypes()(Code) | | |
| getJumpCount | | public int getJumpCount()(Code) | | |
| getRelativePosition | | public Position getRelativePosition()(Code) | | Returns the relative position (number of blank heading lines and
columns) of the primary token of this element.
To get the relative position of the syntactical first token,
call the corresponding method of getFirstElement().
the relative position of the primary token. |
| getStartPosition | | public Position getStartPosition()(Code) | | Returns the start position of the primary token of this element.
To get the start position of the syntactical first token,
call the corresponding method of getFirstElement().
the start position of the primary token. |
| visit | | public void visit(Visitor v)(Code) | | calls the corresponding method of a visitor in order to
perform some action/transformation on this element
Parameters:
v - the Visitor |
|
|