|
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 VariableAccess | |
escjava.ast | |
escjava.translate | |
javafe.ast |
Uses of VariableAccess in escjava.ast |
Fields in escjava.ast declared as VariableAccess | |
VariableAccess |
DecreasesInfo.fOld
|
VariableAccess |
AssignCmd.v
|
Methods in escjava.ast with parameters of type VariableAccess | |
static SubSubGetsCmd |
SubSubGetsCmd.make(VariableAccess v,
Expr rhs,
Expr index1,
Expr index2)
|
static SubGetsCmd |
SubGetsCmd.make(VariableAccess v,
Expr rhs,
Expr index)
|
static RestoreFromCmd |
RestoreFromCmd.make(VariableAccess v,
Expr rhs)
|
static GetsCmd |
GetsCmd.make(VariableAccess v,
Expr rhs)
|
Constructors in escjava.ast with parameters of type VariableAccess | |
DecreasesInfo(int loc,
Expr f,
VariableAccess fOld)
|
Uses of VariableAccess in escjava.translate |
Fields in escjava.translate declared as VariableAccess | |
(package private) VariableAccess |
InvariantInfo.s
|
static VariableAccess |
TrAnExpr.currentAlloc
|
static VariableAccess |
TrAnExpr.currentState
|
static VariableAccess |
GC.allocvar
|
static VariableAccess |
GC.ecvar
|
static VariableAccess |
GC.elemsvar
|
static VariableAccess |
GC.resultvar
|
static VariableAccess |
GC.xresultvar
|
static VariableAccess |
GC.objectTBCvar
|
static VariableAccess |
GC.statevar
|
static VariableAccess |
GC.LSvar
|
static VariableAccess |
GC.thisvar
|
Methods in escjava.translate that return VariableAccess | |
private VariableAccess |
Translate.adorn(VariableAccess v)
Make a fresh version of a special variable to save it in. |
private VariableAccess |
Translate.initadorn(LocalVarDecl d)
Make a fresh "boolean" variable to hold the initialized status of a Java variable that is marked as "uninitialized". |
private static VariableAccess |
Translate.getInitVar(GenericVarDecl d)
Return the VariableAccesss associated with d by a
call to setInitVar . |
private VariableAccess |
Translate.fresh(VarInit e,
int loc)
Generate a temporary for the result of a given expression. |
private VariableAccess |
Translate.fresh(VarInit e,
int loc,
java.lang.String suffix)
|
private VariableAccess |
Translate.temporary(java.lang.String s,
int locAccess)
Generate a temporary variable with prefix s and associated
expression location information locAccess . |
private VariableAccess |
Translate.temporary(java.lang.String s,
int locAccess,
int locIdDecl)
|
VariableAccess |
Translate.cacheValue(Expr e)
|
(package private) static VariableAccess |
TrAnExpr.tempName(int loc,
java.lang.String prefix,
Type type)
|
static VariableAccess |
TrAnExpr.makeVarAccess(GenericVarDecl decl,
int loc)
|
protected static VariableAccess |
TrAnExpr.apply(java.util.Hashtable map,
VariableAccess va)
|
static VariableAccess |
TrAnExpr.stateVar(java.util.Hashtable sp)
|
private VariableAccess |
InitialState.addMapping(GenericVarDecl vd)
|
private static VariableAccess |
GetSpec.shave(Expr e)
Shaves a GC designator. |
(package private) static VariableAccess |
GetSpec.createVarVariant(GenericVarDecl vd,
java.lang.String postfix)
* Given a GenericVarDecl named "x@old", returns a VariableAccess to a * fresh LocalVarDecl named "x@ |
static VariableAccess |
GC.makeVar(Identifier name,
int locId)
|
static VariableAccess |
GC.makeVar(java.lang.String name,
int locId)
|
static VariableAccess |
GC.makeFormalPara(java.lang.String name,
Type type,
int locId)
|
static VariableAccess |
GC.makeVar(java.lang.String name)
|
static VariableAccess |
GC.makeVar(Identifier name)
|
static VariableAccess |
GC.makeFormalPara(java.lang.String name,
Type type)
|
static VariableAccess |
GC.makeFormalPara(java.lang.String name)
|
Methods in escjava.translate with parameters of type VariableAccess | |
static LocalVarDecl |
UniqName.newIntermediateStateVar(VariableAccess v,
java.lang.String suffix)
Returns a new intermediate-state variable associated with an existing VariableAccess. |
private VariableAccess |
Translate.adorn(VariableAccess v)
Make a fresh version of a special variable to save it in. |
private static Expr |
Translate.predEvathangsAnArray(VariableAccess allocOld,
VariableAccess allocNew)
Returns the guarded-command expression: (FORALL o :: ! |
private static Expr |
Translate.predArrayOwnerNull(VariableAccess allocOld,
VariableAccess allocNew,
VariableAccess arr)
Returns the guarded-command expression: (FORALL o :: ! |
private static void |
Translate.setInitVar(GenericVarDecl d,
VariableAccess init)
Associates init with d ; will be returned by a call
to getInitVar . |
private GuardedCmd |
Translate.modify(VariableAccess va,
int loc)
Modifies a GC designator. |
protected static VariableAccess |
TrAnExpr.apply(java.util.Hashtable map,
VariableAccess va)
|
static GuardedCmd |
GC.gets(VariableAccess lhs,
Expr rhs)
|
static GuardedCmd |
GC.subgets(VariableAccess lhs,
Expr index,
Expr rhs)
|
static GuardedCmd |
GC.subsubgets(VariableAccess lhs,
Expr array,
Expr index,
Expr rhs)
|
static GuardedCmd |
GC.restoreFrom(VariableAccess lhs,
Expr rhs)
|
Uses of VariableAccess in javafe.ast |
Methods in javafe.ast that return VariableAccess | |
static VariableAccess |
VariableAccess.make(Identifier id,
int loc,
GenericVarDecl decl)
|
Methods in javafe.ast with parameters of type VariableAccess | |
java.lang.Object |
VisitorArgResult.visitVariableAccess(VariableAccess x,
java.lang.Object o)
|
void |
Visitor.visitVariableAccess(VariableAccess x)
|
void |
DefaultVisitor.visitVariableAccess(VariableAccess x)
|
|
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 |