|
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 StackVector | |
escjava.ast | |
escjava.pa | |
escjava.tc | |
escjava.translate | |
javafe.ast | |
javafe.parser | |
javafe.tc |
Uses of StackVector in escjava.ast |
Methods in escjava.ast with parameters of type StackVector | |
static VarExprModifierPragmaVec |
VarExprModifierPragmaVec.popFromStackVector(StackVector s)
|
static ModifiesGroupPragmaVec |
ModifiesGroupPragmaVec.popFromStackVector(StackVector s)
|
static LocalVarDeclVec |
LocalVarDeclVec.popFromStackVector(StackVector s)
|
static GuardedCmdVec |
GuardedCmdVec.popFromStackVector(StackVector s)
|
static GenericVarDeclVec |
GenericVarDeclVec.popFromStackVector(StackVector s)
|
static ExprStmtPragmaVec |
ExprStmtPragmaVec.popFromStackVector(StackVector s)
|
static ExprModifierPragmaVec |
ExprModifierPragmaVec.popFromStackVector(StackVector s)
|
static ExprDeclPragmaVec |
ExprDeclPragmaVec.popFromStackVector(StackVector s)
|
static DefPredVec |
DefPredVec.popFromStackVector(StackVector s)
|
static DecreasesInfoVec |
DecreasesInfoVec.popFromStackVector(StackVector s)
|
static ConditionVec |
ConditionVec.popFromStackVector(StackVector s)
|
static CondExprModifierPragmaVec |
CondExprModifierPragmaVec.popFromStackVector(StackVector s)
|
Uses of StackVector in escjava.pa |
Fields in escjava.pa declared as StackVector | |
private StackVector |
PredicateAbstraction.code
|
Uses of StackVector in escjava.tc |
Fields in escjava.tc declared as StackVector | |
protected StackVector |
PrepTypeDeclaration.jmlFieldsSeq
|
protected StackVector |
PrepTypeDeclaration.jmlHiddenFieldsSeq
|
protected StackVector |
PrepTypeDeclaration.jmlDupFieldsSeq
|
Uses of StackVector in escjava.translate |
Fields in escjava.translate declared as StackVector | |
private StackVector |
Translate.code
Contains the guarded commands generated so far for the current method. |
private StackVector |
Translate.declaredLocals
Contains the local Java variables declared in the current block so far for the current block and enclosing blocks of the current method. |
private StackVector |
Translate.temporaries
Contains the temporaries that generated for the current method that haven't yet been declared in a VARINCMD. |
Methods in escjava.translate with parameters of type StackVector | |
private static void |
GetSpec.addAssumptions(ExprVec ev,
StackVector code)
Appends code with an assume C command for
every condition C in cv . |
private static void |
GetSpec.assumeConditions(ConditionVec cv,
StackVector code)
|
private static void |
GetSpec.checkConditions(ConditionVec cv,
int loc,
StackVector code)
Appends code with an check loc: C command for
every condition C in cv . |
private static void |
GetSpec.checkModifiesConstraints(Spec spec,
FindContributors scope,
Set syntargets,
java.util.Hashtable premap,
int loc,
StackVector code)
|
static GuardedCmd |
GC.boxPopFromStackVector(StackVector s)
Pops two command sequences off s , call them a
and b . |
Uses of StackVector in javafe.ast |
Uses of StackVector in javafe.parser |
Fields in javafe.parser declared as StackVector | |
protected StackVector |
ParseUtil.seqModifierPragma
|
protected StackVector |
ParseType.seqIdentifier
|
protected StackVector |
ParseStmt.seqStmt
Internal working storage for many ParseStmt
functions. |
protected StackVector |
ParseStmt.seqCatchClause
|
protected StackVector |
ParseExpr.seqExpr
Internal working storage for parseNewExpression, parseExpressionList, and ParseStmt.parseForStmt functions. |
protected StackVector |
ParseExpr.seqVarInit
Internal working storage for parseArrayInitializer function. |
protected StackVector |
ParseExpr.seqTypeDeclElem
Internal working storage for parseNewExpression function. |
protected StackVector |
Parse.seqTypeName
Internal working storage for many Parse functions. |
protected StackVector |
Parse.seqFormalParaDecl
Internal working storage for many Parse functions. |
protected StackVector |
Parse.seqImportDecl
Internal working storage for many Parse functions. |
protected StackVector |
Parse.seqTypeDecl
Internal working storage for many Parse functions. |
Uses of StackVector in javafe.tc |
Fields in javafe.tc declared as StackVector | |
protected StackVector |
PrepTypeDeclaration.fieldSeq
|
protected StackVector |
PrepTypeDeclaration.hiddenfieldSeq
|
protected StackVector |
PrepTypeDeclaration.methodSeq
|
protected StackVector |
PrepTypeDeclaration.constructorSeq
|
Methods in javafe.tc with parameters of type StackVector | |
static TypeSigVec |
TypeSigVec.popFromStackVector(StackVector s)
|
|
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 |