|
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 ModifiesGroupPragmaVec | |
escjava.ast | |
escjava.translate |
Uses of ModifiesGroupPragmaVec in escjava.ast |
Fields in escjava.ast declared as ModifiesGroupPragmaVec | |
ModifiesGroupPragmaVec |
DerivedMethodDecl.modifies
|
Methods in escjava.ast that return ModifiesGroupPragmaVec | |
static ModifiesGroupPragmaVec |
ModifiesGroupPragmaVec.make()
* Public maker methods: * * |
static ModifiesGroupPragmaVec |
ModifiesGroupPragmaVec.make(int count)
|
static ModifiesGroupPragmaVec |
ModifiesGroupPragmaVec.make(java.util.Vector vec)
|
static ModifiesGroupPragmaVec |
ModifiesGroupPragmaVec.make(ModifiesGroupPragma[] els)
|
static ModifiesGroupPragmaVec |
ModifiesGroupPragmaVec.popFromStackVector(StackVector s)
|
ModifiesGroupPragmaVec |
ModifiesGroupPragmaVec.copy()
|
Methods in escjava.ast with parameters of type ModifiesGroupPragmaVec | |
void |
ModifiesGroupPragmaVec.append(ModifiesGroupPragmaVec vec)
|
Uses of ModifiesGroupPragmaVec in escjava.translate |
Methods in escjava.translate that return ModifiesGroupPragmaVec | |
private static ModifiesGroupPragmaVec |
GetSpec.filterModifies(ModifiesGroupPragmaVec mvec,
FindContributors scope)
|
Methods in escjava.translate with parameters of type ModifiesGroupPragmaVec | |
private static ModifiesGroupPragmaVec |
GetSpec.filterModifies(ModifiesGroupPragmaVec mvec,
FindContributors scope)
|
private Expr |
Frame.modifiesCheckFieldHelper(Expr eod,
int callLoc,
FieldDecl fd,
int calleeLoc,
Expr callee_tprecondition,
boolean genExpr,
ModifiesGroupPragmaVec mg,
Expr thisexpr,
java.util.Hashtable args)
This is a helper method to generate checks that a particular field assignment is allowed by the frame conditions. |
(package private) void |
Frame.modifiesCheckMethodI(ModifiesGroupPragmaVec calleeFrameConditions,
Expr eod,
int loccall,
java.util.Hashtable args,
boolean freshResult,
TypeDecl td_callee)
This method generates checks that the locations possibly assigned by a called method are allowed to be assigned by the caller. |
private Expr |
Frame.modifiesCheckMethod(Expr eod,
int loccall,
java.util.Hashtable args,
boolean freshResult,
java.lang.Object calleeStoreRef,
Expr callee_tprecondition,
boolean genExpr,
ModifiesGroupPragmaVec mg)
Helper method that checks that a particular store-ref in the frame conditions of a called method against the frame conditions of the caller. |
private Expr |
Frame.modifiesCheckArray(Expr array,
Expr arrayIndex,
int callLoc,
int calleeLoc,
Expr callee_tprecondition,
boolean genExpr,
ModifiesGroupPragmaVec mg,
Expr thisexpr,
java.util.Hashtable args)
This adds checks for whether the given array with the given index may be assigned to. |
|
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 |