|
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 GenericVarDecl | |
escjava.ast | |
escjava.backpred | |
escjava.pa | |
escjava.parser | |
escjava.sp | |
escjava.tc | |
escjava.translate | |
javafe.ast | |
javafe.tc |
Uses of GenericVarDecl in escjava.ast |
Fields in escjava.ast declared as GenericVarDecl | |
GenericVarDecl |
VarExprModifierPragma.arg
|
GenericVarDecl |
SubstExpr.var
|
private GenericVarDecl[] |
GenericVarDeclVec.elements
* Instance fields: * * |
Methods in escjava.ast that return GenericVarDecl | |
GenericVarDecl |
GenericVarDeclVec.elementAt(int index)
* Other methods: * * |
GenericVarDecl[] |
GenericVarDeclVec.toArray()
|
GenericVarDecl |
GenericVarDeclVec.pop()
|
Methods in escjava.ast with parameters of type GenericVarDecl | |
static VarExprModifierPragma |
VarExprModifierPragma.make(int tag,
GenericVarDecl arg,
Expr expr,
int loc)
|
static ModifierPragma |
Utils.findModifierPragma(GenericVarDecl vdecl,
int tag)
Finds and returns the first modifier pragma of vdecl
that has the tag tag , if any. |
static void |
Utils.removeModifierPragma(GenericVarDecl vdecl,
int tag)
|
static SubstExpr |
SubstExpr.make(int sloc,
int eloc,
GenericVarDecl var,
Expr val,
Expr target)
|
static GenericVarDeclVec |
GenericVarDeclVec.make(GenericVarDecl[] els)
|
void |
GenericVarDeclVec.setElementAt(GenericVarDecl x,
int index)
|
boolean |
GenericVarDeclVec.contains(GenericVarDecl x)
|
void |
GenericVarDeclVec.addElement(GenericVarDecl x)
|
boolean |
GenericVarDeclVec.removeElement(GenericVarDecl x)
|
void |
GenericVarDeclVec.insertElementAt(GenericVarDecl obj,
int index)
|
void |
EscPrettyPrint.exsuresPrintDecl(java.io.OutputStream o,
GenericVarDecl d)
|
Constructors in escjava.ast with parameters of type GenericVarDecl | |
GenericVarDeclVec(GenericVarDecl[] els)
* Private constructors: * * |
Uses of GenericVarDecl in escjava.backpred |
Methods in escjava.backpred with parameters of type GenericVarDecl | |
private void |
FindContributors.backedgeToGenericVarDecl(GenericVarDecl decl,
FieldDeclVec fields,
boolean addTypes,
java.util.LinkedList visited)
Calculate the fields and types "mentioned" by a backedge to a GenericVarDecl and then add them as per walk(,,). |
private static void |
BackPred.genFinalInitInfo(VarInit initExpr,
GenericVarDecl sDecl,
Expr s,
Expr x,
Type type,
int loc,
java.io.PrintStream proverStream)
|
private static void |
BackPred.produce(GenericVarDecl sDecl,
Expr s,
Expr e,
java.io.PrintStream proverStream)
|
Uses of GenericVarDecl in escjava.pa |
Methods in escjava.pa with parameters of type GenericVarDecl | |
private static boolean |
PredicateAbstraction.mentions(Expr e,
GenericVarDecl d)
|
Uses of GenericVarDecl in escjava.parser |
Subclasses of GenericVarDecl in escjava.parser | |
class |
OldVarDecl
|
Uses of GenericVarDecl in escjava.sp |
Methods in escjava.sp with parameters of type GenericVarDecl | |
VarMap |
VarMap.extend(GenericVarDecl v,
Expr e)
Returns a VarMap identical to "this", except mapping "v" to "e". |
Expr |
VarMap.get(GenericVarDecl v)
|
Uses of GenericVarDecl in escjava.tc |
Fields in escjava.tc declared as GenericVarDecl | |
protected GenericVarDecl |
EnvForGhostLocals.decl
The new local binding. |
Constructors in escjava.tc with parameters of type GenericVarDecl | |
EnvForGhostLocals(Env parent,
GenericVarDecl decl)
Create a environment from an existing one by adding a new local binding. |
Uses of GenericVarDecl in escjava.translate |
Fields in escjava.translate declared as GenericVarDecl | |
(package private) GenericVarDecl |
ParamAndGlobalVarInfo.vdecl
|
(package private) static GenericVarDecl |
Inner.firstThis0
* If non-null, the local variable or formal to use instead of * this.this$0 when unfolding |
GenericVarDecl |
ATarget.x
|
Methods in escjava.translate with parameters of type GenericVarDecl | |
protected void |
VcToStringPvs.printVarDecl(java.io.PrintStream out,
GenericVarDecl decl)
|
protected void |
VcToString.printVarDecl(java.io.PrintStream out,
GenericVarDecl decl)
|
static LocalVarDecl |
UniqName.newIntermediateStateVar(GenericVarDecl vd,
java.lang.String suffix)
|
static java.lang.String |
UniqName.variable(GenericVarDecl v)
Returns the unique-ification of the variable v . |
private static java.lang.String |
UniqName.verifyUnique(GenericVarDecl o,
java.lang.String s)
|
private static VariableAccess |
Translate.getInitVar(GenericVarDecl d)
Return the VariableAccesss associated with d by a
call to setInitVar . |
private static void |
Translate.setInitVar(GenericVarDecl d,
VariableAccess init)
Associates init with d ; will be returned by a call
to getInitVar . |
static Expr |
TrAnExpr.targetTypeCorrect(GenericVarDecl vd,
java.util.Hashtable wt)
This method implements the ESCJ 16 function TargetTypeCorrect ,
except for the init$ case! |
static Expr |
TrAnExpr.typeCorrect(GenericVarDecl vd)
This method implements the ESCJ 16 function TypeCorrect . |
static Expr |
TrAnExpr.typeCorrect(GenericVarDecl vd,
java.util.Hashtable sp)
|
static Expr |
TrAnExpr.quantTypeCorrect(GenericVarDecl vd,
java.util.Hashtable sp)
|
static Expr |
TrAnExpr.resultEqualsCall(GenericVarDecl vd,
RoutineDecl rd,
java.util.Hashtable sp)
|
static Expr |
TrAnExpr.typeCorrectAs(GenericVarDecl vd,
Type type)
|
static Expr |
TrAnExpr.typeAndNonNullCorrectAs(GenericVarDecl vd,
Type type,
SimpleModifierPragma nonNullPragma,
boolean forceNonNull,
java.util.Hashtable sp)
|
static ExprVec |
TrAnExpr.typeAndNonNullAllocCorrectAs(GenericVarDecl vd,
Type type,
SimpleModifierPragma nonNullPragma,
boolean forceNonNull,
java.util.Hashtable sp,
boolean mentionAllocated)
Returns a vector of conjuncts. |
static Expr |
TrAnExpr.elemsTypeCorrect(GenericVarDecl edecl)
|
static VariableAccess |
TrAnExpr.makeVarAccess(GenericVarDecl decl,
int loc)
|
private static java.util.ArrayList |
TrAnExpr.makeBounds(RoutineDecl rd,
GenericVarDecl newThis)
|
private VariableAccess |
InitialState.addMapping(GenericVarDecl vd)
|
(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@ |
private static void |
GetSpec.addFreeTypeCorrectAs(GenericVarDecl vd,
Type type,
ConditionVec cv)
Adds to cv a condition stating that vd has
type type . |
private static void |
GetSpec.setNonNullPragma(GenericVarDecl v,
SimpleModifierPragma nonnull)
* Mark v as non_null because of non_null pragma nonnull. * * Precondition: nonnull is a NON_NULL pragma. * * (Used to implement inheritence of non_null's.) |
static SimpleModifierPragma |
GetSpec.NonNullPragma(GenericVarDecl v)
* Has a particular declaration been declared non_null? |
static SimpleModifierPragma |
GetSpec.superNonNullPragma(GenericVarDecl v)
Returns non-null if the formal parameter is declared non-null in some overridden declaration of the method. |
static Expr |
GC.subst(int sloc,
int eloc,
GenericVarDecl var,
Expr val,
Expr target)
|
static Expr |
GC.subst(GenericVarDecl var,
Expr val,
Expr target)
|
static Expr |
GC.forall(GenericVarDecl v,
Expr e)
|
static Expr |
GC.forall(GenericVarDecl v,
Expr range,
Expr e)
|
static Expr |
GC.forall(GenericVarDecl v,
Expr e,
ExprVec nopats)
|
static Expr |
GC.forallwithpats(GenericVarDecl v,
Expr e,
ExprVec pats)
|
static Expr |
GC.forall(int sloc,
int eloc,
GenericVarDecl v,
Expr range,
Expr e)
|
static Expr |
GC.forall(int sloc,
int eloc,
GenericVarDecl v,
Expr range,
Expr e,
ExprVec nopats)
|
static Expr |
GC.quantifiedExpr(int sloc,
int eloc,
int tag,
GenericVarDecl v,
Expr range,
Expr e,
ExprVec nopats,
ExprVec pats)
|
private static void |
ATarget.addTarget(GenericVarDecl vd)
|
private static void |
ATarget.addTarget(GenericVarDecl vd,
Expr index)
|
private static void |
ATarget.addTarget(GenericVarDecl vd,
Expr index1,
Expr index2)
|
private static void |
ATarget.addTarget(GenericVarDecl vd,
Expr[] indices)
|
private static void |
ATarget.extendEnv(java.util.Hashtable env,
GenericVarDecl d,
Expr e)
|
Constructors in escjava.translate with parameters of type GenericVarDecl | |
ATarget(GenericVarDecl x,
Expr[] indices)
|
Uses of GenericVarDecl in javafe.ast |
Subclasses of GenericVarDecl in javafe.ast | |
class |
FieldDecl
Represents a field declaration. |
class |
FormalParaDecl
Represents a FormalParameter. |
class |
LocalVarDecl
Represents a LocalVariableDeclarationStatement. |
Fields in javafe.ast declared as GenericVarDecl | |
GenericVarDecl |
VariableAccess.decl
|
Methods in javafe.ast with parameters of type GenericVarDecl | |
java.lang.Object |
VisitorArgResult.visitGenericVarDecl(GenericVarDecl x,
java.lang.Object o)
|
void |
Visitor.visitGenericVarDecl(GenericVarDecl x)
|
static VariableAccess |
VariableAccess.make(Identifier id,
int loc,
GenericVarDecl decl)
|
void |
StandardPrettyPrint.print(java.io.OutputStream o,
GenericVarDecl d)
|
abstract void |
PrettyPrint.print(java.io.OutputStream o,
GenericVarDecl d)
|
java.lang.String |
PrettyPrint.toString(GenericVarDecl d)
|
void |
DelegatingPrettyPrint.print(java.io.OutputStream o,
GenericVarDecl d)
|
void |
DefaultVisitor.visitGenericVarDecl(GenericVarDecl x)
|
Uses of GenericVarDecl in javafe.tc |
Fields in javafe.tc declared as GenericVarDecl | |
protected GenericVarDecl |
EnvForLocals.decl
The new local binding. |
Methods in javafe.tc with parameters of type GenericVarDecl | |
static TypeSig |
Env.whereDeclared(GenericVarDecl decl)
What type is a GenericVarDecl declared in? |
Constructors in javafe.tc with parameters of type GenericVarDecl | |
EnvForLocals(Env parent,
GenericVarDecl decl)
Create a environment from an existing one by adding a new local binding. |
|
EnvForLocals(Env parent,
GenericVarDecl decl,
boolean warnAboutDuplication)
|
|
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 |