|
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 FieldDecl | |
escjava | |
escjava.ast | |
escjava.backpred | |
escjava.parser | |
escjava.tc | |
escjava.translate | |
javafe.ast | |
javafe.parser | |
javafe.reader | |
javafe.tc |
Uses of FieldDecl in escjava |
Methods in escjava with parameters of type FieldDecl | |
(package private) void |
RefinementSequence.combineFields(FieldDecl newfd,
FieldDecl fd)
|
Uses of FieldDecl in escjava.ast |
Fields in escjava.ast declared as FieldDecl | |
FieldDecl |
ModelDeclPragma.decl
|
FieldDecl |
GhostDeclPragma.decl
|
Methods in escjava.ast with parameters of type FieldDecl | |
static boolean |
Utils.isModel(FieldDecl fd)
|
static ModelDeclPragma |
ModelDeclPragma.make(FieldDecl decl,
int loc)
|
static GhostDeclPragma |
GhostDeclPragma.make(FieldDecl decl,
int loc)
|
Uses of FieldDecl in escjava.backpred |
Methods in escjava.backpred with parameters of type FieldDecl | |
private void |
FindContributors.addField(FieldDecl fd)
Add a given field to contributorFields, maintaining all the closure properties. |
private void |
FindContributors.addPossibleMentions(FieldDecl fd,
ExprDeclPragma J)
Add the mapping (fd, J) to fieldToPossible. |
Uses of FieldDecl in escjava.parser |
Methods in escjava.parser that return FieldDecl | |
FieldDecl |
EscPragmaParser.isPragmaDecl(Token l)
|
FieldDecl |
ErrorPragmaParser.isPragmaDecl(Token l)
|
Uses of FieldDecl in escjava.tc |
Methods in escjava.tc that return FieldDecl | |
FieldDecl |
TypeSig.lookupField(Identifier id,
TypeSig caller)
|
FieldDecl |
GhostEnv.getGhostField(java.lang.String n,
FieldDecl excluded)
Attempts to find a ghost or model field that belongs to us (including supertypes) with name n that is not equal to excluded , which may
be null . |
Methods in escjava.tc with parameters of type FieldDecl | |
FieldDecl |
GhostEnv.getGhostField(java.lang.String n,
FieldDecl excluded)
Attempts to find a ghost or model field that belongs to us (including supertypes) with name n that is not equal to excluded , which may
be null . |
static boolean |
GhostEnv.isStatic(FieldDecl d)
|
static boolean |
GhostEnv.isGhostField(FieldDecl field)
Determines if a field is a ghost (not model or Java) field |
static java.util.List |
Datagroups.get(TypeDecl td,
FieldDecl fd)
Get the items that are in the datagroup for fd |
static void |
Datagroups.add(TypeDecl td,
FieldDecl fd,
Expr fa)
Add Expr fa to the datagroup for declaration fd in the context of type td; the declaration fd may be in a superclass. |
Uses of FieldDecl in escjava.translate |
Methods in escjava.translate that return FieldDecl | |
static FieldDecl |
Inner.getEnclosingInstanceField(TypeSig T)
* Return the FieldDecl for a given non-top-level TypeSig's * enclosing instance field (this$0). |
Methods in escjava.translate with parameters of type FieldDecl | |
static Expr |
TrAnExpr.fieldTypeCorrect(FieldDecl fdecl)
|
static ExprVec |
TrAnExpr.getModelVarAxioms(TypeDecl td,
FieldDecl fd,
java.util.Hashtable sp)
|
static TypeDeclElemVec |
GetSpec.getRepresentsClauses(TypeDecl td,
FieldDecl fd)
Gets the represents clauses for a model field fd as seen from a type declaration td; fd may be declared in td or in a supertype of td. |
boolean |
Frame.isDefinitelyNotAssignable(Expr eod,
FieldDecl fd)
This method returns whether the given field (fd) of the given object (eod) (which is null if the field is static) is definitely not allowed to be assigned according to the specs of the current RoutineDecl. |
(package private) void |
Frame.modifiesCheckField(Expr lhs,
int callLoc,
FieldDecl fd)
This method generates checks that the field in lhs is allowed to be assigned according to the specification of the current RoutineDecl (rdCurrent). |
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. |
private void |
Frame.ModifiesIterator.add(ObjectDesignator od,
FieldDecl d)
Adds the contents of the datagroup d (of object od, which may not be null) to the 'others' list. |
private int |
Frame.ModifiesIterator.count(FieldDecl d)
Returns the number of times the argument is in the 'done' list |
Constructors in escjava.translate with parameters of type FieldDecl | |
RepHelper(TypeDecl td,
FieldDecl fd)
|
Uses of FieldDecl in javafe.ast |
Fields in javafe.ast declared as FieldDecl | |
private FieldDecl[] |
FieldDeclVec.elements
* Instance fields: * * |
FieldDecl |
FieldAccess.decl
|
Methods in javafe.ast that return FieldDecl | |
FieldDecl |
FieldDeclVec.elementAt(int index)
* Other methods: * * |
FieldDecl[] |
FieldDeclVec.toArray()
|
FieldDecl |
FieldDeclVec.pop()
|
static FieldDecl |
FieldDecl.make(int modifiers,
ModifierPragmaVec pmodifiers,
Identifier id,
Type type,
int locId,
VarInit init,
int locAssignOp)
|
Methods in javafe.ast with parameters of type FieldDecl | |
java.lang.Object |
VisitorArgResult.visitFieldDecl(FieldDecl x,
java.lang.Object o)
|
void |
Visitor.visitFieldDecl(FieldDecl x)
|
void |
StandardPrettyPrint.print(java.io.OutputStream o,
int ind,
FieldDecl d,
boolean showBody)
|
abstract void |
PrettyPrint.print(java.io.OutputStream o,
int ind,
FieldDecl d,
boolean showBody)
|
java.lang.String |
PrettyPrint.toString(FieldDecl d,
boolean showBody)
|
static FieldDeclVec |
FieldDeclVec.make(FieldDecl[] els)
|
void |
FieldDeclVec.setElementAt(FieldDecl x,
int index)
|
boolean |
FieldDeclVec.contains(FieldDecl x)
|
void |
FieldDeclVec.addElement(FieldDecl x)
|
boolean |
FieldDeclVec.removeElement(FieldDecl x)
|
void |
FieldDeclVec.insertElementAt(FieldDecl obj,
int index)
|
void |
DelegatingPrettyPrint.print(java.io.OutputStream o,
int ind,
FieldDecl d,
boolean showBody)
|
void |
DefaultVisitor.visitFieldDecl(FieldDecl x)
|
Constructors in javafe.ast with parameters of type FieldDecl | |
FieldDeclVec(FieldDecl[] els)
* Private constructors: * * |
Uses of FieldDecl in javafe.parser |
Methods in javafe.parser that return FieldDecl | |
FieldDecl |
PragmaParser.isPragmaDecl(Token l)
|
Uses of FieldDecl in javafe.reader |
Fields in javafe.reader declared as FieldDecl | |
private FieldDecl[] |
ASTClassFileParser.fields
The fields of the class being parsed. |
Uses of FieldDecl in javafe.tc |
Fields in javafe.tc declared as FieldDecl | |
static FieldDecl |
Types.lengthFieldDecl
|
Methods in javafe.tc that return FieldDecl | |
FieldDecl |
TypeSig.lookupField(Identifier id,
TypeSig caller)
TBW |
static FieldDecl |
Types.lookupField(Type t,
Identifier id,
TypeSig caller)
|
protected FieldDecl |
Types.lookupFieldInstance(Type t,
Identifier id,
TypeSig caller)
|
Methods in javafe.tc with parameters of type FieldDecl | |
protected void |
PrepTypeDeclaration.visitFieldDecl(FieldDecl x,
TypeSig currentSig,
boolean abstractMethodsOK,
boolean inFinalClass,
boolean inInterface)
Visit a FieldDecl, check it and add it to fieldSeq. |
void |
FlowInsensitiveChecks.checkFieldDecl(FieldDecl fd)
Moves fd into implementation checked state. |
|
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 |