Object
- VarInfoName

All Implemented Interfaces:

Serializable, Comparable<VarInfoName>

Direct Known Subclasses:

VarInfoName.Add, VarInfoName.Elements, VarInfoName.Field, VarInfoName.FunctionOf, VarInfoName.FunctionOfN, VarInfoName.Poststate, VarInfoName.Prestate, VarInfoName.Simple, VarInfoName.SizeOf, VarInfoName.Slice, VarInfoName.Subscript, VarInfoName.TypeOf
```
@Interned
public abstract class VarInfoName
extends Object
implements Serializable, Comparable<VarInfoName>
```
VarInfoName represents the "name" of a variable. Calling it a "name", however, is somewhat misleading. It can be some expression that includes more than one variable, term, etc. We separate this from the VarInfo itself because clients wish to manipulate names into new expressions independent of the VarInfo that they might be associated with. VarInfoName's child classes are specific types of names, like applying a function to something. For example, "a" is a name, and "sin(a)" is a name that is the name "a" with the function "sin" applied to it.

See Also:

Serialized Form

Nested Class Summary

Nested Classes
Modifier and Type	Class	Description
`static class`	`VarInfoName.AbstractVisitor<T>`	Traverse the tree elements that have exactly one branch (so the traversal order doesn't matter).
`static class`	`VarInfoName.Add`	An integer amount more or less than some other value, like "x+2".
`static class`	`VarInfoName.BooleanAndVisitor`
`static class`	`VarInfoName.Elements`	The elements of a container, like "term[]".
`static class`	`VarInfoName.ElementsFinder`	Use to traverse a tree, find the first (elements ...) node, and report whether it's in pre or post-state.
`static class`	`VarInfoName.Field`	A 'getter' operation for some field, like a.foo.
`static class`	`VarInfoName.Finder`	Finds if a given VarInfoName is contained in a set of nodes in the VarInfoName tree using == comparison.
`static class`	`VarInfoName.FunctionOf`	A function over a term, like "sum(argument)".
`static class`	`VarInfoName.FunctionOfN`	A function of multiple parameters.
`static class`	`VarInfoName.InorderFlattener`	Use to collect all elements in a tree into an inorder-traversal list.
`static class`	`VarInfoName.Intersection`	Intersection of two sequences.
`static class`	`VarInfoName.IsAllNonPoststateVisitor`
`static class`	`VarInfoName.IsAllPrestateVisitor`
`static class`	`VarInfoName.LexicalComparator`	Compare VarInfoNames alphabetically.
`static class`	`VarInfoName.NodeFinder`	Use to report whether a node is in a pre- or post-state context.
`static class`	`VarInfoName.NoReturnValue`
`static class`	`VarInfoName.PostPreConverter`	Replace pre states by normal variables, and normal variables by post states.
`static class`	`VarInfoName.Poststate`	The poststate value of a term, like "new(term)".
`static class`	`VarInfoName.Prestate`	The prestate value of a term, like "orig(term)" or "\old(term)".
`static class`	`VarInfoName.QuantHelper`	Helper for writing parts of quantification expressions.
`static class`	`VarInfoName.QuantifierVisitor`	A quantifier visitor can be used to search a tree and return all unquantified sequences (e.g.
`static class`	`VarInfoName.Replacer`	A Replacer is a Visitor that makes a copy of a tree, but replaces some node (and its children) with another.
`static class`	`VarInfoName.Simple`	A simple identifier like "a", etc.
`static class`	`VarInfoName.SimpleNamesVisitor`
`static class`	`VarInfoName.SizeOf`	The size of a contained sequence; form is like "size(sequence)" or "sequence.length".
`static class`	`VarInfoName.Slice`	A slice of elements from a sequence, like "sequence[i..j]".
`static class`	`VarInfoName.Subscript`	An element from a sequence, like "sequence[index]".
`static interface`	`VarInfoName.Transformer`	Specifies a function that performs a transformation on VarInfoNames.
`static class`	`VarInfoName.TypeOf`	The type of the term, like "term.getClass().getName()" or "\typeof(term)".
`static class`	`VarInfoName.Union`	Union of two sequences.
`static interface`	`VarInfoName.Visitor<T>`	Visitor framework for processing of VarInfoNames.

Field Summary

Fields
Modifier and Type	Field	Description
`static Logger`	`debug`	Debugging Logger.
`static boolean`	`dkconfig_direct_orig`	When true, apply orig directly to variables, do not apply orig to derived variables.
`static VarInfoName.Transformer`	`IDENTITY_TRANSFORMER`	A pass-through transformer.
`static VarInfoName`	`ORIG_THIS`
`static boolean`	`testCall`
`static VarInfoName`	`THIS`
`static VarInfoName`	`ZERO`

Constructor Summary

Constructors
Constructor Description

VarInfoName()

Method Summary

All Methods Static Methods Instance Methods Abstract Methods Concrete Methods
Modifier and Type	Method	Description
`abstract <T> T`	`accept(VarInfoName.Visitor<T> v)`	Accept the actions of a visitor.
`VarInfoName`	`applyAdd(int amount)`	Returns a name for the this term plus a constant, like "this-1" or "this+1".
`VarInfoName`	`applyDecrement()`	Returns a name for the decrement of this term, like "this-1".
`VarInfoName`	`applyElements()`	Returns a name for the elements of a container (as opposed to the identity of the container) like "this[]" or "(elements this)".
`VarInfoName`	`applyField(String field)`	Returns a 'getter' operation for some field of this name, like a.foo if this is a.
`VarInfoName`	`applyFunction(String function)`	Returns a name for a unary function applied to this object.
`static VarInfoName`	`applyFunctionOfN(String function, @Interned VarInfoName[] vars)`	Returns a name for a function of more than one argument.
`static VarInfoName`	`applyFunctionOfN(String function, List<VarInfoName> vars)`	Returns a name for a function applied to more than one argument.
`VarInfoName`	`applyIncrement()`	Returns a name for the increment of this term, like "this+1".
`VarInfoName`	`applyIntersection(VarInfoName seq2)`	Returns a name for the intersection of with another sequence, like "intersect(a[], b[])".
`VarInfoName`	`applyPoststate()`	Returns a name for a the poststate value of this object; form is like "new(this)" or "\new(this)".
`VarInfoName`	`applyPrestate()`	Returns a name for a the prestate value of this object; form is like "orig(this)" or "\old(this)".
`VarInfoName`	`applySize()`	Returns a name for the size of this (this object should be a sequence).
`VarInfoName`	`applySlice(@Nullable VarInfoName i, @Nullable VarInfoName j)`	Returns a name for a slice of element selected from a sequence, like "this[i..j]".
`VarInfoName`	`applySubscript(VarInfoName index)`	Returns a name for an element selected from a sequence, like "this[i]".
`VarInfoName`	`applyTypeOf()`	Returns a name for the type of this object; form is like "this.getClass().getName()" or "\typeof(this)".
`VarInfoName`	`applyUnion(VarInfoName seq2)`	Returns a name for the union of this with another sequence, like "union(a[], b[])".
`int`	`compareTo(VarInfoName other)`
`@Interned String`	`dbc_name(VarInfo var)`	Return the String representation of this name in the dbc style output format.
`protected abstract String`	`dbc_name_impl(VarInfo v)`	Return the name in the DBC style output format.
`boolean`	`equals(@GuardSatisfied @Nullable Object o)`
`boolean`	`equalsVarInfoName(@GuardSatisfied VarInfoName other)`
`@Interned String`	`esc_name()`	Return the String representation of this name in the esc style output format.
`protected abstract String`	`esc_name_impl()`	Returns the String representation of this name in the ESC style output format.
`@Interned VarInfoName[]`	`getSliceBounds()`	If this is a slice, (potentially in pre-state), return its lower and upper bounds, which can be subtracted to get one less than its size.
`int`	`hashCode()`
`boolean`	`hasNode(VarInfoName node)`	Returns true iff the given node can be found in this.
`boolean`	`hasNodeOfType(Class<?> type)`	Returns true iff a node of the given type exists in this.
`boolean`	`hasTypeOf()`	Returns true iff a TypeOf node exists in this.
`@Interned String`	`identifier_name()`	Return the String representation of this name using only letters, numbers, and underscores.
`protected abstract String`	`identifier_name_impl()`	Returns the name using only letters, numbers, and underscores.
`boolean`	`includesSimpleName(String name)`	Returns true if this VarInfoName contains a simple variable whose name is NAME.
`Collection<VarInfoName>`	`inOrderTraversal()`	Returns the nodes of this, as given by an inorder traversal.
`boolean`	`inPrestateContext(VarInfoName node)`	Returns true if the given node is in a prestate context within this tree.
`VarInfoName`	`intern()`
`boolean`	`isAllPrestate()`	Returns true if every variable in the name is an orig(...) variable.
`boolean`	`isApplySizeSafe()`	Returns true iff applySize will not throw an exception.
`boolean`	`isLiteralConstant()`	Returns true when this is "0", "-1", "1", etc.
`boolean`	`isThis()`	Returns whether or not this name refers to the 'this' variable of a class.
`@Interned String`	`java_name(VarInfo v)`	Return the String representation of this name in the java style output format.
`protected abstract String`	`java_name_impl(VarInfo v)`	Return the String representation of this name in java format.
`@Interned String`	`jml_name(VarInfo v)`	Return the String representation of this name in the JML style output format.
`protected abstract String`	`jml_name_impl(VarInfo v)`	Returns the name in JML style output format.
`VarInfoName`	`JMLElementCorrector()`
`@Interned String`	`name()`	Return the String representation of this name in the default output format.
`protected abstract String`	`name_impl()`	Returns the String representation of this name in the default output format.
`String`	`name_using(OutputFormat format, VarInfo vi)`	Returns name of this in the specified format.
`static VarInfoName`	`parse(String name)`	Given the standard String representation of a variable name (like what appears in the normal output format), return the corresponding VarInfoName.
`VarInfoName`	`replace(VarInfoName node, VarInfoName replacement)`	Replace the first instance of node by replacement, in the data structure rooted at this.
`VarInfoName`	`replaceAll(VarInfoName node, VarInfoName replacement)`	Replace all instances of node by replacement, in the data structure rooted at this.
`String`	`repr()`	Returns the name, in a debugging format.
`protected abstract String`	`repr_impl()`	Returns the name in a verbose debugging format.
`@Interned String`	`simplify_name()`	Returns the string representation (interned) of this name, in the Simplify tool output format in the pre-state context.
`protected @Interned String`	`simplify_name(boolean prestate)`	Returns the string representation (interned) of this name, in the Simplify tool output format, in the given pre/post-state context.
`protected abstract String`	`simplify_name_impl(boolean prestate)`	Returns the String representation of this name in the simplify output format in either prestate or poststate context.
`String`	`toString()`

Methods inherited from class Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait

- Field Detail
  - debug
```
public static Logger debug
```
    Debugging Logger.
  - dkconfig_direct_orig
```
public static boolean dkconfig_direct_orig
```
    When true, apply orig directly to variables, do not apply orig to derived variables. For example, create 'size(orig(a[]))' rather than 'orig(size(a[]))'.
  - testCall
```
public static boolean testCall
```
  - ZERO
```
public static final VarInfoName ZERO
```
  - THIS
```
public static final VarInfoName THIS
```
  - ORIG_THIS
```
public static final VarInfoName ORIG_THIS
```
  - IDENTITY_TRANSFORMER
```
public static final VarInfoName.Transformer IDENTITY_TRANSFORMER
```
    A pass-through transformer.
- Constructor Detail
  - VarInfoName
```
public VarInfoName()
```
- Method Detail
  - parse
```
public static VarInfoName parse(String name)
```
    Given the standard String representation of a variable name (like what appears in the normal output format), return the corresponding VarInfoName. This method can't parse all the strings that the VarInfoName name() method might produce, but it should be able to handle anything that appears in a decls file. Specifically, it can only handle a subset of the grammar of derived variables. For some values of "name", "name.equals(parse(e.name()))" might throw an exception, but if it completes normally, the result should be true.
  - name
```
@Pure
public @Interned String name(@GuardSatisfied VarInfoName this)
```
    Return the String representation of this name in the default output format.
    
    Returns:
    
    the string representation (interned) of this name, in the default output format
  - name_impl
```
protected abstract String name_impl(@GuardSatisfied VarInfoName this)
```
    Returns the String representation of this name in the default output format. Result is not interned; the client (name()) does so, then caches the interned value.
  - esc_name
```
public @Interned String esc_name()
```
    Return the String representation of this name in the esc style output format.
    
    Returns:
    
    the string representation (interned) of this name, in the esc style output format
  - esc_name_impl
```
protected abstract String esc_name_impl()
```
    Returns the String representation of this name in the ESC style output format. Cached by esc_name().
  - simplify_name
```
public @Interned String simplify_name()
```
    Returns the string representation (interned) of this name, in the Simplify tool output format in the pre-state context.
    
    Returns:
    
    the string representation (interned) of this name, in the Simplify tool output format in the pre-state context
  - simplify_name
```
protected @Interned String simplify_name(boolean prestate)
```
    Returns the string representation (interned) of this name, in the Simplify tool output format, in the given pre/post-state context.
    
    Parameters:
    
    prestate - if true, return the variable in a prestate context; if false, return the variable in a poststate context
    
    Returns:
    
    the string representation (interned) of this name, in the Simplify tool output format, in the given pre/post-state context
  - simplify_name_impl
```
protected abstract String simplify_name_impl(boolean prestate)
```
    Returns the String representation of this name in the simplify output format in either prestate or poststate context.
  - java_name
```
public @Interned String java_name(VarInfo v)
```
    Return the String representation of this name in the java style output format.
    
    Returns:
    
    the string representation (interned) of this name, in the java style output format
  - java_name_impl
```
protected abstract String java_name_impl(VarInfo v)
```
    Return the String representation of this name in java format. Cached and interned by java_name(daikon.VarInfo).
  - jml_name
```
public @Interned String jml_name(VarInfo v)
```
    Return the String representation of this name in the JML style output format.
  - jml_name_impl
```
protected abstract String jml_name_impl(VarInfo v)
```
    Returns the name in JML style output format. Cached and interned by jml_name(daikon.VarInfo).
  - dbc_name
```
public @Interned String dbc_name(VarInfo var)
```
    Return the String representation of this name in the dbc style output format.
    
    Parameters:
    
    var - the VarInfo which goes along with this VarInfoName. Used to determine the type of the variable.
    If var is null, the only repercussion is that if `this' is an "orig(x)" expression, it will be formatted in jml-style, something like "\old(x)".
    If var is not null and `this' is an "orig(x)" expressions, it will be formatted in Jtest's DBC style, as "$pre(type, x)".
    
    Returns:
    
    the string representation (interned) of this name, in the dbc style output format
  - dbc_name_impl
```
protected abstract String dbc_name_impl(VarInfo v)
```
    Return the name in the DBC style output format. If v is null, uses JML style instead. Cached and interned by dbc_name(daikon.VarInfo).
  - identifier_name
```
public @Interned String identifier_name()
```
    Return the String representation of this name using only letters, numbers, and underscores.
  - identifier_name_impl
```
protected abstract String identifier_name_impl()
```
    Returns the name using only letters, numbers, and underscores. Cached and interned by identifier_name().
    
    Returns:
    
    the name using only letters, numbers, and underscores
  - name_using
```
public String name_using(OutputFormat format,
                         VarInfo vi)
```
    Returns name of this in the specified format.
    
    Parameters:
    
    format - the format in which to return this variable name
    
    vi - the VarInfo for this variable name
    
    Returns:
    
    name of this in the specified format
  - repr
```
public String repr(@GuardSatisfied @UnknownSignedness VarInfoName this)
```
    Returns the name, in a debugging format.
    
    Returns:
    
    the name, in a debugging format
  - repr_impl
```
protected abstract String repr_impl(@GuardSatisfied @UnknownSignedness VarInfoName this)
```
    Returns the name in a verbose debugging format. Cached by repr().
    
    Returns:
    
    the name in a verbose debugging format
  - intern
```
@InternMethod
public VarInfoName intern()
```
  - isLiteralConstant
```
@Pure
public boolean isLiteralConstant()
```
    Returns true when this is "0", "-1", "1", etc.
    
    Returns:
    
    true when this is "0", "-1", "1", etc
  - inOrderTraversal
```
public Collection<VarInfoName> inOrderTraversal(@Interned VarInfoName this)
```
    Returns the nodes of this, as given by an inorder traversal.
    
    Returns:
    
    the nodes of this, as given by an inorder traversal
  - hasNode
```
public boolean hasNode(VarInfoName node)
```
    Returns true iff the given node can be found in this. If the node has children, the whole subtree must match.
    
    Parameters:
    
    node - a variable name
    
    Returns:
    
    true iff the given node can be found in this. If the node has children, the whole subtree must match
  - hasNodeOfType
```
public boolean hasNodeOfType(Class<?> type)
```
    Returns true iff a node of the given type exists in this.
    
    Parameters:
    
    type - the type to search for
    
    Returns:
    
    true iff a node of the given type exists in this
  - hasTypeOf
```
public boolean hasTypeOf()
```
    Returns true iff a TypeOf node exists in this.
    
    Returns:
    
    true iff a TypeOf node exists in this
  - isThis
```
@Pure
public boolean isThis()
```
    Returns whether or not this name refers to the 'this' variable of a class. True for both normal and prestate versions of the variable.
  - inPrestateContext
```
public boolean inPrestateContext(@Interned VarInfoName this,
                                 VarInfoName node)
```
    Returns true if the given node is in a prestate context within this tree.
    
    Parameters:
    
    node - a member of this tree
    
    Returns:
    
    true if the given node is in a prestate context within this tree
  - isAllPrestate
```
@Pure
public boolean isAllPrestate(@Interned VarInfoName this)
```
    Returns true if every variable in the name is an orig(...) variable.
    
    Returns:
    
    true if every variable in the name is an orig(...) variable
  - includesSimpleName
```
public boolean includesSimpleName(@Interned VarInfoName this,
                                  String name)
```
    Returns true if this VarInfoName contains a simple variable whose name is NAME.
    
    Parameters:
    
    name - the name to search for in this VarInfoName
    
    Returns:
    
    true if this VarInfoName contains a simple variable whose name is NAME
  - replace
```
public VarInfoName replace(@Interned VarInfoName this,
                           VarInfoName node,
                           VarInfoName replacement)
```
    Replace the first instance of node by replacement, in the data structure rooted at this.
  - replaceAll
```
public VarInfoName replaceAll(@Interned VarInfoName this,
                              VarInfoName node,
                              VarInfoName replacement)
```
    Replace all instances of node by replacement, in the data structure rooted at this.
  - equals
```
@EnsuresNonNullIf(result=true,
                  expression="#1")
@Pure
public boolean equals(@GuardSatisfied VarInfoName this,
                      @GuardSatisfied @Nullable Object o)
```
    Overrides:
    
    equals in class Object
  - equalsVarInfoName
```
@EnsuresNonNullIf(result=true,
                  expression="#1")
@Pure
public boolean equalsVarInfoName(@GuardSatisfied @Interned VarInfoName this,
                                 @GuardSatisfied VarInfoName other)
```
  - hashCode
```
@Pure
public int hashCode(@GuardSatisfied @UnknownSignedness VarInfoName this)
```
    Overrides:
    
    hashCode in class Object
  - compareTo
```
@Pure
public int compareTo(@GuardSatisfied VarInfoName this,
                     VarInfoName other)
```
    Specified by:
    
    compareTo in interface Comparable<VarInfoName>
  - toString
```
@SideEffectFree
public String toString(@GuardSatisfied VarInfoName this)
```
    Overrides:
    
    toString in class Object
  - isApplySizeSafe
```
@Pure
public boolean isApplySizeSafe()
```
    Returns true iff applySize will not throw an exception.
    
    Returns:
    
    true iff applySize will not throw an exception
    
    See Also:
    
    applySize()
  - applySize
```
public VarInfoName applySize(@Interned VarInfoName this)
```
    Returns a name for the size of this (this object should be a sequence). Form is like "size(a[])" or "a.length".
    
    Returns:
    
    a name for the size of this
  - getSliceBounds
```
public @Interned VarInfoName[] getSliceBounds(@Interned VarInfoName this)
```
    If this is a slice, (potentially in pre-state), return its lower and upper bounds, which can be subtracted to get one less than its size.
  - applyFunction
```
public VarInfoName applyFunction(@Interned VarInfoName this,
                                 String function)
```
    Returns a name for a unary function applied to this object. The result is like "sum(this)".
    
    Parameters:
    
    function - the function to apply
    
    Returns:
    
    a name for the function applied to this
  - applyFunctionOfN
```
public static VarInfoName applyFunctionOfN(String function,
                                           List<VarInfoName> vars)
```
    Returns a name for a function applied to more than one argument. The result is like "sum(var1, var2)".
    
    Parameters:
    
    function - the name of the function
    
    vars - the arguments to the function, of type VarInfoName
    
    Returns:
    
    a name for a function applied to multiple arguments
  - applyFunctionOfN
```
public static VarInfoName applyFunctionOfN(String function,
                                           @Interned VarInfoName[] vars)
```
    Returns a name for a function of more than one argument. The result is like "sum(var1, var2)".
    
    Parameters:
    
    function - the name of the function
    
    vars - the arguments to the function
  - applyIntersection
```
public VarInfoName applyIntersection(@Interned VarInfoName this,
                                     VarInfoName seq2)
```
    Returns a name for the intersection of with another sequence, like "intersect(a[], b[])".
    
    Parameters:
    
    seq2 - the variable to intersect with
    
    Returns:
    
    the name for the intersection of this and seq2
  - applyUnion
```
public VarInfoName applyUnion(@Interned VarInfoName this,
                              VarInfoName seq2)
```
    Returns a name for the union of this with another sequence, like "union(a[], b[])".
    
    Parameters:
    
    seq2 - the variable to union with
    
    Returns:
    
    the name for the intersection of this and seq2
  - applyField
```
public VarInfoName applyField(@Interned VarInfoName this,
                              String field)
```
    Returns a 'getter' operation for some field of this name, like a.foo if this is a.
    
    Parameters:
    
    field - the field
    
    Returns:
    
    the name for the given field of this
  - applyTypeOf
```
public VarInfoName applyTypeOf(@Interned VarInfoName this)
```
    Returns a name for the type of this object; form is like "this.getClass().getName()" or "\typeof(this)".
    
    Returns:
    
    the name for the type of this object
  - applyPrestate
```
public VarInfoName applyPrestate(@Interned VarInfoName this)
```
    Returns a name for a the prestate value of this object; form is like "orig(this)" or "\old(this)".
  - applyPoststate
```
public VarInfoName applyPoststate(@Interned VarInfoName this)
```
    Returns a name for a the poststate value of this object; form is like "new(this)" or "\new(this)".
    
    Returns:
    
    the name for the poststate value of this object
  - applyAdd
```
public VarInfoName applyAdd(@Interned VarInfoName this,
                            int amount)
```
    Returns a name for the this term plus a constant, like "this-1" or "this+1".
  - applyDecrement
```
public VarInfoName applyDecrement(@Interned VarInfoName this)
```
    Returns a name for the decrement of this term, like "this-1".
  - applyIncrement
```
public VarInfoName applyIncrement(@Interned VarInfoName this)
```
    Returns a name for the increment of this term, like "this+1".
  - applyElements
```
public VarInfoName applyElements(@Interned VarInfoName this)
```
    Returns a name for the elements of a container (as opposed to the identity of the container) like "this[]" or "(elements this)".
    
    Returns:
    
    the name for the elements of this container
  - applySubscript
```
public VarInfoName applySubscript(@Interned VarInfoName this,
                                  VarInfoName index)
```
    Returns a name for an element selected from a sequence, like "this[i]".
  - applySlice
```
public VarInfoName applySlice(@Interned VarInfoName this,
                              @Nullable VarInfoName i,
                              @Nullable VarInfoName j)
```
    Returns a name for a slice of element selected from a sequence, like "this[i..j]". If an endpoint is null, it means "from the start" or "to the end".
  - accept
```
public abstract <T> T accept(VarInfoName.Visitor<T> v)
```
    Accept the actions of a visitor.
  - JMLElementCorrector
```
public VarInfoName JMLElementCorrector()
```

Class VarInfoName

Nested Class Summary

Field Summary

Constructor Summary

Method Summary

Methods inherited from class Object

Field Detail

debug

dkconfig_direct_orig

testCall

ZERO

THIS

ORIG_THIS

IDENTITY_TRANSFORMER

Constructor Detail

VarInfoName

Method Detail

parse

name

name_impl

esc_name

esc_name_impl

simplify_name

simplify_name

simplify_name_impl

java_name

java_name_impl

jml_name

jml_name_impl

dbc_name

dbc_name_impl

identifier_name

identifier_name_impl

name_using

repr

repr_impl

intern

isLiteralConstant

inOrderTraversal

hasNode

hasNodeOfType

hasTypeOf

isThis

inPrestateContext

isAllPrestate

includesSimpleName

replace

replaceAll

equals

equalsVarInfoName

hashCode

compareTo

toString

isApplySizeSafe

applySize

getSliceBounds

applyFunction

applyFunctionOfN

applyFunctionOfN

applyIntersection

applyUnion

applyField

applyTypeOf

applyPrestate

applyPoststate

applyAdd

applyDecrement

applyIncrement

applyElements

applySubscript

applySlice

accept

JMLElementCorrector