|
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 TypeDecl | |
escjava | |
escjava.ast | |
escjava.backpred | |
escjava.gui | |
escjava.parser | |
escjava.tc | |
escjava.translate | |
javafe | |
javafe.ast | |
javafe.parser | |
javafe.reader | |
javafe.tc |
Uses of TypeDecl in escjava |
Fields in escjava declared as TypeDecl | |
private TypeDecl |
RefinementSequence.objectDecl
|
protected TypeDecl |
AnnotationHandler.td
|
Methods in escjava that return TypeDecl | |
(package private) TypeDecl |
RefinementSequence.getObjectDecl()
|
(package private) TypeDecl |
RefinementSequence.cleancopy(TypeDecl td)
|
Methods in escjava with parameters of type TypeDecl | |
(package private) void |
RefinementSequence.combineType(TypeDecl newtd,
TypeDecl td,
boolean addNewItems)
|
(package private) MethodDecl |
RefinementSequence.findMatchingMethod(MethodDecl md,
TypeDecl td)
|
(package private) TypeDecl |
RefinementSequence.cleancopy(TypeDecl td)
|
void |
Main.handleTD(TypeDecl td)
This method is called by SrcTool on the TypeDecl of each outside type that SrcTool is to process. |
private boolean |
Main.processTD(TypeDecl td)
Run all the requested stages on a given TypeDecl; return true if we had to abort. |
void |
AnnotationHandler.handleTypeDecl(TypeDecl td)
After parsing, but before type checking, we need to convert model methods to regular methods, so that names are resolved correctly; also need to set ACC_PURE bits correctly in all classes so that later checks get done correctly. |
void |
AnnotationHandler.desugar(TypeDecl td)
|
void |
AnnotationHandler.NestedPragmaParser.parseAllRoutineSpecs(TypeDecl td)
|
Uses of TypeDecl in escjava.ast |
Fields in escjava.ast declared as TypeDecl | |
TypeDecl |
ModelTypePragma.decl
|
Methods in escjava.ast that return TypeDecl | |
TypeDecl |
DerivedMethodDecl.getContainingClass()
|
Methods in escjava.ast with parameters of type TypeDecl | |
static boolean |
Utils.isImmutable(TypeDecl cd)
|
void |
ModelTypePragma.setParent(TypeDecl p)
|
static ModelTypePragma |
ModelTypePragma.make(TypeDecl decl,
int loc)
|
void |
ModelMethodDeclPragma.setParent(TypeDecl p)
|
void |
ModelDeclPragma.setParent(TypeDecl p)
|
void |
ModelConstructorDeclPragma.setParent(TypeDecl p)
|
void |
GhostDeclPragma.setParent(TypeDecl p)
|
Uses of TypeDecl in escjava.backpred |
Methods in escjava.backpred with parameters of type TypeDecl | |
private void |
FindContributors.walkInstanceInitialier(TypeDecl td,
FieldDeclVec fields,
boolean addTypes,
java.util.LinkedList visited)
Walk the implicit instance initializer code for a given TypeDecl, excluding any field initializations of superinterface fields. |
protected static void |
BackPred.addContribution(TypeDecl d,
java.io.PrintStream proverStream)
Add to b the contribution from a particular TypeDecl, which is a formula. |
private static void |
BackPred.saySuper(TypeDecl d,
java.io.PrintStream proverStream)
|
Uses of TypeDecl in escjava.gui |
Fields in escjava.gui declared as TypeDecl | |
TypeDecl |
GUI.TDTreeValue.td
|
Methods in escjava.gui with parameters of type TypeDecl | |
void |
GUI.createTDNode(TypeDecl td,
javax.swing.tree.DefaultMutableTreeNode cunode)
|
static javax.swing.tree.DefaultMutableTreeNode |
GUI.TDTreeValue.makeNode(TypeDecl td)
|
Constructors in escjava.gui with parameters of type TypeDecl | |
GUI.TDTreeValue(TypeDecl td)
|
Uses of TypeDecl in escjava.parser |
Methods in escjava.parser that return TypeDecl | |
protected TypeDecl |
EscPragmaParser.parseTypeDeclTail(Lex l,
boolean specOnly,
int loc,
int modifiers,
ModifierPragmaVec modifierPragmas)
|
Uses of TypeDecl in escjava.tc |
Methods in escjava.tc with parameters of type TypeDecl | |
protected TypeSig |
Types.makeTypeSigInstance(java.lang.String simpleName,
Env enclosingEnv,
TypeDecl decl)
|
protected TypeSig |
Types.makeTypeSigInstance(java.lang.String[] packageName,
java.lang.String simpleName,
TypeSig enclosingType,
TypeDecl decl,
CompilationUnit cu)
|
void |
PrepTypeDeclaration.prepStart(TypeSig sig,
TypeDecl decl)
|
void |
PrepTypeDeclaration.prepEnd(TypeSig sig,
TypeDecl decl)
|
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. |
static java.util.Map |
Datagroups.initMap(TypeDecl td)
|
static java.util.Map |
Datagroups.getMap(TypeDecl td)
|
Constructors in escjava.tc with parameters of type TypeDecl | |
TypeSig(java.lang.String[] packageName,
java.lang.String simpleName,
TypeSig enclosingType,
TypeDecl decl,
CompilationUnit CU)
|
|
TypeSig(java.lang.String simpleName,
Env enclosingEnv,
TypeDecl decl)
|
Uses of TypeDecl in escjava.translate |
Fields in escjava.translate declared as TypeDecl | |
private TypeDecl |
Translate.typeDecl
The type containing the routine whose body is being translated. |
TypeDecl |
RepHelper.td
|
private TypeDecl |
Frame.ModifiesIterator.td
The TypeDecl whose view of any datagroups is to be used. |
Methods in escjava.translate with parameters of type TypeDecl | |
private TypeExpr |
Translate.getClassObject(TypeDecl tdClass)
|
private void |
Translate.instanceInitializers(TypeDecl tdecl)
This method implements "InstanceInitializers", as described in section 8.1 of ESCJ 16. |
private void |
Translate.instanceInitializeZero(TypeDecl tdecl)
Called by instanceInitializers . |
private void |
Translate.trStmt(Stmt stmt,
TypeDecl decl)
Translate stmt into a sequence of guarded commands
that are appended to code .
|
private void |
Translate.trIfStmt(Expr guard,
Stmt thenStmt,
Stmt elseStmt,
TypeDecl decl)
Translate an "if" statement. |
private void |
Translate.trSynchronizedBody(Expr mu,
Stmt stmt,
int loc,
TypeDecl decl)
|
static ExprVec |
TrAnExpr.getModelVarAxioms(TypeDecl td,
FieldDecl fd,
java.util.Hashtable sp)
|
static void |
InlineConstructor.inlineConstructorsInAllMethods(TypeDecl td)
|
private static void |
InlineConstructor.createMethodDecl(MethodDecl md,
TypeDecl td,
ConstructorDecl cd,
Identifier newThis,
int count)
|
static ConditionVec |
GetSpec.addConstraintClauses(ConditionVec post,
TypeDecl decl,
java.util.Hashtable wt,
ExprVec postAssumptions)
|
private static void |
GetSpec.nonNullInitChecks(TypeDecl td,
ConditionVec post)
Add to post all NonNullInit checks for non_null instance
fields and instance ghost fields declared in td . |
private static void |
GetSpec.addSuperInterfaces(TypeDecl td,
Set set)
|
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. |
(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. |
Constructors in escjava.translate with parameters of type TypeDecl | |
RepHelper(TypeDecl td,
FieldDecl fd)
|
|
RepHelper(TypeDecl td,
RoutineDecl rd)
|
|
Frame.ModifiesIterator(TypeDecl td,
CondExprModifierPragmaVec mp,
boolean expandDatagroups)
Creates an iterator over the store-ref locations in the CondExprModifierPragmaVec. |
|
Frame.ModifiesIterator(TypeDecl td,
CondExprModifierPragmaVec mp,
boolean expandDatagroups,
boolean expandWild)
Creates an iterator over the store-ref locations in the CondExprModifierPragmaVec. |
Uses of TypeDecl in javafe |
Methods in javafe with parameters of type TypeDecl | |
void |
TestTool.handleTD(TypeDecl td)
This method is called on the TypeDecl of each outside type that SrcTool is to process. |
TypeSig |
TestTool.getSuperClass(TypeDecl td)
Attempt to fetch the TypeSig for a given
TypeDecl . |
void |
SrcTool.handleTD(TypeDecl td)
This method is called on the TypeDecl of each outside type that SrcTool is to process. |
void |
PrintSpec.PrintSpecPrettyPrint.printnoln(java.io.OutputStream o,
int ind,
TypeDecl d)
|
void |
CopyLoaded.handleTD(TypeDecl td)
Called from handleCU on each TypeDecl from the CU's loaded from the program files. |
private boolean |
CopyLoaded.processTD(TypeDecl td)
Typecheck a TypeDecl; return true if we had to abort. |
Uses of TypeDecl in javafe.ast |
Subclasses of TypeDecl in javafe.ast | |
class |
ClassDecl
|
class |
InterfaceDecl
|
Fields in javafe.ast declared as TypeDecl | |
private TypeDecl[] |
TypeDeclVec.elements
* Instance fields: * * |
TypeDecl |
TypeDeclElemPragma.parent
|
TypeDecl |
TypeDecl.parent
|
TypeDecl |
RoutineDecl.parent
|
TypeDecl |
InitBlock.parent
|
TypeDecl |
FieldDecl.parent
|
Methods in javafe.ast that return TypeDecl | |
TypeDecl |
TypeDeclVec.elementAt(int index)
* Other methods: * * |
TypeDecl[] |
TypeDeclVec.toArray()
|
TypeDecl |
TypeDeclVec.pop()
|
TypeDecl |
TypeDeclElemPragma.getParent()
|
TypeDecl |
TypeDeclElem.getParent()
The TypeDecl we are an element of, or null if we do not have a parent (cf. hasParent). |
TypeDecl |
TypeDecl.getParent()
|
TypeDecl |
RoutineDecl.getParent()
|
TypeDecl |
InitBlock.getParent()
|
TypeDecl |
FieldDecl.getParent()
|
Methods in javafe.ast with parameters of type TypeDecl | |
java.lang.Object |
VisitorArgResult.visitTypeDecl(TypeDecl x,
java.lang.Object o)
|
void |
Visitor.visitTypeDecl(TypeDecl x)
|
static TypeDeclVec |
TypeDeclVec.make(TypeDecl[] els)
|
void |
TypeDeclVec.setElementAt(TypeDecl x,
int index)
|
boolean |
TypeDeclVec.contains(TypeDecl x)
|
void |
TypeDeclVec.addElement(TypeDecl x)
|
boolean |
TypeDeclVec.removeElement(TypeDecl x)
|
void |
TypeDeclVec.insertElementAt(TypeDecl obj,
int index)
|
void |
TypeDeclElemPragma.setParent(TypeDecl p)
|
void |
TypeDeclElem.setParent(TypeDecl p)
|
void |
TypeDecl.setParent(TypeDecl p)
|
void |
StandardPrettyPrint.printnoln(java.io.OutputStream o,
int ind,
TypeDecl d)
|
void |
RoutineDecl.setParent(TypeDecl p)
|
void |
PrettyPrint.print(java.io.OutputStream o,
int ind,
TypeDecl d)
Print a type declaration onto to a stream. |
abstract void |
PrettyPrint.printnoln(java.io.OutputStream o,
int ind,
TypeDecl d)
Print a type declaration onto to a stream, without a final newline. |
void |
InitBlock.setParent(TypeDecl p)
|
void |
FieldDecl.setParent(TypeDecl p)
|
void |
DelegatingPrettyPrint.printnoln(java.io.OutputStream o,
int ind,
TypeDecl d)
|
void |
DefaultVisitor.visitTypeDecl(TypeDecl x)
|
Constructors in javafe.ast with parameters of type TypeDecl | |
TypeDeclVec(TypeDecl[] els)
* Private constructors: * * |
Uses of TypeDecl in javafe.parser |
Methods in javafe.parser that return TypeDecl | |
(package private) abstract TypeDecl |
ParseStmt.parseTypeDeclTail(Lex l,
boolean specOnly,
int loc,
int modifiers,
ModifierPragmaVec modifierPragmas)
Parse a type declaration stating at the class/interface keyword. |
protected TypeDecl |
Parse.parseTypeDeclaration(Lex l,
boolean specOnly)
Parse a TypeDeclaration (ie a class or interface declaration). |
protected TypeDecl |
Parse.parseTypeDeclaration(Lex l,
boolean specOnly,
int modifiers,
ModifierPragmaVec modifierPragmas,
int loc)
|
protected TypeDecl |
Parse.parseTypeDeclTail(Lex l,
boolean specOnly,
int loc,
int modifiers,
ModifierPragmaVec modifierPragmas)
Parse a TypeDeclTail (ie a class or interface declaration starting at the keyword 'class' or 'interface'). |
Uses of TypeDecl in javafe.reader |
Fields in javafe.reader declared as TypeDecl | |
TypeDecl |
ASTClassFileParser.typeDecl
The AST of the class parsed by this parser. |
Uses of TypeDecl in javafe.tc |
Fields in javafe.tc declared as TypeDecl | |
protected TypeDecl |
TypeSig.myTypeDecl
Our TypeDecl; may be null only for package-member type because of laziness. |
protected TypeDecl |
EnvForLocalType.decl
The new local binding. |
Methods in javafe.tc that return TypeDecl | |
TypeDecl |
TypeSig.getTypeDecl()
Get the non-null TypeDecl we are associated with. |
Methods in javafe.tc with parameters of type TypeDecl | |
static TypeSig |
TypeSig.getSig(TypeDecl d)
The myTypeDecl field maps TypeSigs to TypeDecls. |
protected void |
TypeSig.setDecl(TypeDecl decl,
CompilationUnit CU)
Protected routine used to associate a TypeSig with a TypeDecl. |
(package private) void |
TypeSig.load(TypeDecl decl,
CompilationUnit CU)
Load the non-null TypeDecl decl as our TypeDecl. |
static TypeSig |
Types.makeTypeSig(java.lang.String simpleName,
Env enclosingEnv,
TypeDecl decl)
Factory method for TypeSig structures |
protected TypeSig |
Types.makeTypeSigInstance(java.lang.String simpleName,
Env enclosingEnv,
TypeDecl decl)
|
protected static TypeSig |
Types.makeTypeSig(java.lang.String[] packageName,
java.lang.String simpleName,
TypeSig enclosingType,
TypeDecl decl,
CompilationUnit CU)
Factory method for TypeSig structures |
protected TypeSig |
Types.makeTypeSigInstance(java.lang.String[] packageName,
java.lang.String simpleName,
TypeSig enclosingType,
TypeDecl decl,
CompilationUnit CU)
|
void |
TypeCheck.checkTypeDecl(TypeDecl td)
Moves td into the checked state. |
TypeSig |
TypeCheck.getSig(TypeDecl d)
Retrieves the TypeSig associated with a particular
TypeDecl . |
protected void |
PrepTypeDeclaration.prepStart(TypeSig sig,
TypeDecl decl)
|
protected void |
PrepTypeDeclaration.prepDo(TypeSig sig,
TypeDecl decl)
|
protected void |
PrepTypeDeclaration.prepEnd(TypeSig sig,
TypeDecl decl)
|
Set |
PrepTypeDeclaration.getOverrides(TypeDecl td,
MethodDecl md)
Returns the set of methods that md overrides, with
md considered to appear in a particular type
td . |
void |
PrepTypeDeclaration.checkTypeModifiers(TypeDecl decl,
TypeSig currentSig,
boolean isClass)
Check that the modifiers of a type are ok. |
Constructors in javafe.tc with parameters of type TypeDecl | |
TypeSig(java.lang.String simpleName,
Env enclosingEnv,
TypeDecl decl)
Create a TypeSig that represents a non-member type. |
|
TypeSig(java.lang.String[] packageName,
java.lang.String simpleName,
TypeSig enclosingType,
TypeDecl decl,
CompilationUnit CU)
Create a TypeSig that represents a member type. |
|
TypeSig(java.lang.String[] packageName,
java.lang.String simpleName,
TypeDecl decl,
CompilationUnit CU)
Create a TypeSig that represents an internal-use-only package-member type. |
|
EnvForLocalType(Env parent,
TypeDecl decl)
Create a environment from an existing one by adding a new local type binding. |
|
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 |