| java.lang.Object
 de.uka.ilkd.key.rule.updatesimplifier.AbstractAssignmentPairLazy
All known Subclasses: de.uka.ilkd.key.rule.updatesimplifier.AssignmentPairLazy, de.uka.ilkd.key.rule.updatesimplifier.QuanAssignmentPairLazy,
| AbstractAssignmentPairLazy | | protected AbstractAssignmentPairLazy(Term update, int locationPos)(Code) | | |
| equalLocations | | public boolean equalLocations(AssignmentPair p)(Code) | | returns true if the location that is updated is equal to location of the
given assignment pair
Parameters:
p - the AssignmentPair whose location is compared true if the location that is updated is equal to location of thegiven assignment pair |
| equals | | public boolean equals(Object o)(Code) | | returns true if the given object equals this one
|
| freeVars | | public SetOfQuantifiableVariable freeVars()(Code) | | |
| getLocationPos | | protected int getLocationPos()(Code) | | |
| hashCode | | public int hashCode()(Code) | | the hashCode of this assignment pair
|
| location | | public Location location()(Code) | | returns the location operator
the location specifying operator |
| locationAsTerm | | public Term locationAsTerm()(Code) | | returns the location
the left side of the assignment |
| locationHashCode | | public int locationHashCode()(Code) | | returns an int fulfilling the usual hashcode properties but without
consideration of the value part of the assignment pair
an int as location hashcode |
| locationSubs | | public Term[] locationSubs()(Code) | | returns the locations sub terms
the left side of the assignment |
| locationSubtermsBegin | | protected int locationSubtermsBegin()(Code) | | |
| locationSubtermsEnd | | protected int locationSubtermsEnd()(Code) | | |
| value | | public Term value()(Code) | | returns the value that is assigned to the location and adds
if necessary (i.e. the static type T of the location as term is not a
supersort) a type cast (T) in front.
the right side of the assignment |
| valuePos | | protected int valuePos()(Code) | | |
| valueUnsafe | | public Term valueUnsafe()(Code) | | returns the value that is assigned to the location
(no implicit casts are added and therefore themethod is not type safe)
You should be sure what you are doing if using this method, otherwise
AbstractAssignmentPairLazy.value the right side of the assignment |
|
|