|
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 NEXT | FRAMES NO FRAMES |
Packages that use LoopCmd | |
escjava.ast | |
escjava.pa | |
escjava.translate |
Uses of LoopCmd in escjava.ast |
Methods in escjava.ast that return LoopCmd | |
static LoopCmd |
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)
|
Methods in escjava.ast with parameters of type LoopCmd | |
java.lang.Object |
VisitorArgResult.visitLoopCmd(LoopCmd x,
java.lang.Object o)
|
void |
Visitor.visitLoopCmd(LoopCmd x)
|
Uses of LoopCmd in escjava.pa |
Methods in escjava.pa with parameters of type LoopCmd | |
(package private) static GuardedCmd |
PredicateAbstraction.abstractLoop(LoopCmd g,
GuardedCmd context,
Set env)
|
private void |
PredicateAbstraction.inferPredicates(LoopCmd g,
Set env,
Set targets)
|
Constructors in escjava.pa with parameters of type LoopCmd | |
PredicateAbstraction(LoopCmd g,
Set env)
|
Uses of LoopCmd in escjava.translate |
Methods in escjava.translate that return LoopCmd | |
static LoopCmd |
GC.loop(int sLoop,
int eLoop,
int locHotspot,
java.util.Hashtable oldmap,
ConditionVec J,
DecreasesInfoVec decs,
LocalVarDeclVec skolemConsts,
ExprVec P,
GenericVarDeclVec tempVars,
GuardedCmd B,
GuardedCmd S)
|
Methods in escjava.translate with parameters of type LoopCmd | |
private void |
Translate.desugarLoopFast(LoopCmd loop,
ExprVec axs)
Desugars loop according to the fast option. |
private void |
Translate.addLoopDecreases(LoopCmd loop,
int piece)
Adds to code the various pieces of the translation of the
decreases pragma. |
void |
Translate.desugarLoopSafe(LoopCmd loop,
ExprVec axs)
Desugars loop according to the safe option. |
private void |
Translate.checkLoopInvariants(LoopCmd loop,
ExprVec axs)
Add to "code" checks for all loop invariants of "loop". |
|
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 NEXT | FRAMES NO FRAMES |