|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectjavafe.ast.ASTNode
escjava.ast.GuardedCmd
escjava.ast.LoopCmd
Field Summary | |
GuardedCmd |
body
|
DecreasesInfoVec |
decreases
|
GuardedCmd |
desugared
|
GuardedCmd |
guard
|
ConditionVec |
invariants
|
int |
locEnd
|
int |
locHotspot
|
int |
locStart
|
java.util.Hashtable |
oldmap
|
ExprVec |
predicates
|
LocalVarDeclVec |
skolemConstants
|
GenericVarDeclVec |
tempVars
|
Fields inherited from class javafe.ast.ASTNode |
|
Constructor Summary | |
protected |
LoopCmd()
Construct a raw LoopCmd whose class invariant(s) have not yet been established. |
Method Summary | |
void |
accept(Visitor v)
Accept a visit from v . |
java.lang.Object |
accept(VisitorArgResult v,
java.lang.Object o)
|
void |
check()
|
java.lang.Object |
childAt(int index)
Return the first-but-ith child of a node. |
int |
childCount()
Return the number of children a node has. |
int |
getEndLoc()
|
int |
getStartLoc()
|
int |
getTag()
Return the tag of a node. |
static LoopCmd |
make(int locStart,
int locEnd,
int locHotspot,
java.util.Hashtable oldmap,
ConditionVec invariants,
DecreasesInfoVec decreases,
LocalVarDeclVec skolemConstants,
ExprVec predicates,
GenericVarDeclVec tempVars,
GuardedCmd guard,
GuardedCmd body)
|
java.lang.String |
toString()
Return a string representation of this .
|
Methods inherited from class javafe.ast.ASTNode |
clone, clone, getDecorations, setDecorations |
Methods inherited from class java.lang.Object |
equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait |
Field Detail |
public int locStart
public int locEnd
public int locHotspot
public java.util.Hashtable oldmap
public ConditionVec invariants
public DecreasesInfoVec decreases
public LocalVarDeclVec skolemConstants
public ExprVec predicates
public GenericVarDeclVec tempVars
public GuardedCmd guard
public GuardedCmd body
public GuardedCmd desugared
Constructor Detail |
protected LoopCmd()
Method Detail |
public int getStartLoc()
getStartLoc
in class ASTNode
public int getEndLoc()
getEndLoc
in class ASTNode
public final int childCount()
GuardedCmd
childCount
in class GuardedCmd
public final java.lang.Object childAt(int index)
GuardedCmd
childAt
in class GuardedCmd
public final java.lang.String toString()
GuardedCmd
this
.
Meant for debugging use only, not for presentation.
toString
in class GuardedCmd
public final int getTag()
GuardedCmd
getTag
in class GuardedCmd
public final void accept(Visitor v)
GuardedCmd
v
. This method simply
calls the method of v
corresponding to the
allocated type of this
, passing this
as the argument. See the design patterns book.
accept
in class GuardedCmd
public final java.lang.Object accept(VisitorArgResult v, java.lang.Object o)
accept
in class GuardedCmd
public void check()
check
in class GuardedCmd
public static LoopCmd make(int locStart, int locEnd, int locHotspot, java.util.Hashtable oldmap, ConditionVec invariants, DecreasesInfoVec decreases, LocalVarDeclVec skolemConstants, ExprVec predicates, GenericVarDeclVec tempVars, GuardedCmd guard, GuardedCmd body)
|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |