| java.lang.Object
 de.uka.ilkd.key.rule.soundness.ProgramSVProxy
| ProgramSVProxy | | public class ProgramSVProxy implements NonTerminalProgramElement,Statement,Expression(Code) | | This class is used to represent atomic statements and expressions. Instances
of this class have no identity themselves, but they are instead provided an
instance of the class ProgramSVSkolem as operator symbol. The
relationship between ProgramSVSkolem and
ProgramSVProxy is similar to the relationship between
Operator and Term
|
| ProgramSVProxy | | public ProgramSVProxy(ProgramSVSkolem p_op, ArrayOfIProgramVariable p_influencingPVs, 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. |
| getInfluencingPVs | | public ArrayOfIProgramVariable getInfluencingPVs()(Code) | | |
| getJumpTable | | public ArrayOfStatement getJumpTable()(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. |
| toString | | public String toString()(Code) | | String representation of the constraint |
| 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 |
|
|