Uses of Class
escjava.ast.LoopCmd

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".