Uses of Class
javafe.ast.ASTNode

Packages that use ASTNode

escjava
escjava.ast
escjava.backpred
escjava.parser
escjava.tc
escjava.translate
escjava.vcGeneration
javafe
javafe.ast
javafe.parser
javafe.tc

Uses of ASTNode in escjava

Subclasses of ASTNode in escjava

static class	AnnotationHandler.NonNullExpr
static class	AnnotationHandler.NullableExpr
class	RefinementSequence

Methods in escjava with parameters of type ASTNode

private void	RefinementSequence.combineUniverses(ASTNode newNode, ASTNode oldNode)
void	AnnotationHandler.CheckPurity.visitNode(ASTNode x, AnnotationHandler.Context cc)

Uses of ASTNode in escjava.ast

Subclasses of ASTNode in escjava.ast

class	AnOverview The files in this package extend the AST classes defined in javafe.ast.
class	ArrayRangeRefExpr
class	AssignCmd
class	Call
class	CmdCmdCmd
class	CondExprModifierPragma
class	Condition
class	DecreasesInfo
class	DefPred
class	DefPredApplExpr
class	DefPredLetExpr
class	DependsPragma
class	DynInstCmd
class	EscPrimitiveType
class	EverythingExpr
class	ExprCmd
class	ExprDeclPragma
class	ExprModifierPragma
class	ExprStmtPragma
class	GCExpr
class	GeneralizedQuantifiedExpr
class	GetsCmd
class	GhostDeclPragma
class	GuardedCmd
class	GuardExpr
class	IdentifierModifierPragma
class	IdExprDeclPragma
class	ImportPragma
class	LabelExpr
class	LockSetExpr
class	LoopCmd
class	MapsExprModifierPragma
class	ModelConstructorDeclPragma
class	ModelDeclPragma
class	ModelMethodDeclPragma
class	ModelProgamModifierPragma
class	ModelTypePragma
class	ModifiesGroupPragma
class	NamedExprDeclPragma
class	NaryExpr
class	NestedModifierPragma
class	NothingExpr
class	NotModifiedExpr
class	NotSpecifiedExpr
class	NowarnPragma
class	NumericalQuantifiedExpr
class	ParsedSpecs
class	QuantifiedExpr
class	ReachModifierPragma
class	RefinePragma
class	ResExpr
class	RestoreFromCmd
class	SeqCmd
class	SetCompExpr
class	SetStmtPragma
class	SimpleCmd
class	SimpleModifierPragma
class	SimpleStmtPragma
class	SkolemConstantPragma
class	Spec
class	StillDeferredDeclPragma
class	SubGetsCmd
class	SubstExpr
class	SubSubGetsCmd
class	TypeExpr
class	VarDeclModifierPragma
class	VarExprModifierPragma
class	VarInCmd
class	WildRefExpr

Methods in escjava.ast with parameters of type ASTNode

void	Utils.BooleanDecoration.set(ASTNode o, boolean b)
boolean	Utils.BooleanDecoration.isTrue(ASTNode o)
abstract boolean	Utils.BooleanDecoration.calculate(ASTNode o)

Uses of ASTNode in escjava.backpred

Methods in escjava.backpred with parameters of type ASTNode

private void	FindContributors.walk(ASTNode N) Walks a given ASTNode, adding all the types it "mentions" via addType and adding all the fields it "mentions" via addField.
private void	FindContributors.walk(ASTNode N, FieldDeclVec fields, boolean addTypes, java.util.LinkedList visited) Walks a given ASTNode, finding all the types it "mentions" and all the fields it "mentions".

Uses of ASTNode in escjava.parser

Subclasses of ASTNode in escjava.parser

class

OldVarDecl

Uses of ASTNode in escjava.tc

Fields in escjava.tc declared as ASTNode

protected ASTNode

FlowInsensitiveChecks.accessibilityContext If accessibilityLowerBound !

Methods in escjava.tc that return ASTNode

ASTNode

EnvForGhostLocals.locateFieldOrLocal(Identifier id) Locate the lexically innermost field or local variable declaration.

Methods in escjava.tc with parameters of type ASTNode

protected Env

FlowInsensitiveChecks.checkModifierPragma(ModifierPragma p, ASTNode ctxt, Env env)

Uses of ASTNode in escjava.translate

Fields in escjava.translate declared as ASTNode

ASTNode

RepHelper.a

Methods in escjava.translate with parameters of type ASTNode

(package private) void	CalcFreeVars.traverse(ASTNode e)
private GuardedCmd	Translate.traceInfoLabelCmd(ASTNode ast, java.lang.String traceInfoTag)
private GuardedCmd	Translate.traceInfoLabelCmd(ASTNode ast, java.lang.String traceInfoTag, int loc)
private void	Translate.addCheck(ASTNode use, int errorName, Expr pred) Calls GC.check to create a check and appends the result to code.
private void	Translate.addCheck(int locUse, int errorName, Expr pred, ASTNode prag) Calls GC.check to create a check and appends the result to code.
(package private) static void	Translate.setop(ASTNode e)
static Set	Substitute.freeVars(ASTNode e) Calculate the free variables of an expression or a GuardedCmd.
private static void	ATarget.computeMentionsSet(ASTNode n, Set s)

Uses of ASTNode in escjava.vcGeneration

Fields in escjava.vcGeneration declared as ASTNode

private ASTNode

VcGenerator.oldRootNode

Methods in escjava.vcGeneration with parameters of type ASTNode

private void	VcGenerator.generateIfpTree(ASTNode n, boolean dot) The main goal of this method is to translate the gc tree (which is still independant from simplify) to a new tree (classes of this new tree are in escjava/vcGeneration which is, by far, easier to manipulate that the one which is given here (parameter e).
private static java.lang.String	VcGenerator.getNameASTNode(ASTNode e) Utility method for creating dot representation of gc tree

Constructors in escjava.vcGeneration with parameters of type ASTNode

VcGenerator(ProverType p, ASTNode e, boolean err, boolean warn, boolean info, boolean colors)

Uses of ASTNode in javafe

Methods in javafe with parameters of type ASTNode

static int

CountLines.count(ASTNode n)

Uses of ASTNode in javafe.ast

Subclasses of ASTNode in javafe.ast

class	AmbiguousMethodInvocation Represents a Name occuring before an argument list.
class	AmbiguousVariableAccess Represents a Name that occurs in an Expression position.
class	ArrayInit Represents an ArrayInitializer.
class	ArrayRefExpr
class	ArrayType
class	AssertStmt
class	BinaryExpr Represents various kinds of binary expressions (eg +,-,|,%=, etc).
class	BlockStmt
class	BranchStmt
class	BreakStmt
class	CastExpr
class	CatchClause
class	ClassDecl
class	ClassDeclStmt
class	ClassLiteral Represents a class literal (Type . class)
class	CompilationUnit The make method of this class has the side effect of pointing the parent pointers of the TypeDecls inside a CompilationUnit to point to that unit.
class	CompoundName
class	CondExpr
class	ConstructorDecl Represents a ConstructorDeclaration.
class	ConstructorInvocation Represents an ExplicitConstructorInvocation.
class	ContinueStmt
class	DoStmt
class	ErrorType Used to indicate the type of an illegal operation, so that error messages do not unnecessarily propagate; should only be used if the error has already been reported.
class	EvalStmt
class	Expr Represents an Expression.
class	ExprObjectDesignator Represents an ObjectDesignator of the form "Expr . ".
class	FieldAccess Represents various kinds of field access expressions.
class	FieldDecl Represents a field declaration.
class	FormalParaDecl Represents a FormalParameter.
class	ForStmt Represents a ForStatement.
class	GenericBlockStmt
class	GenericVarDecl Represents all variable declarations, including field declarations, local variables and formal arguments.
class	IdentifierNode This class is not actually ever an element of an AST.
class	IfStmt
class	ImportDecl
class	InitBlock Represents an initializing block of code as a class member We include modifiers for later extensibility to JDK 1.1, where both static and dynamic initializer blocks are allowed.
class	InstanceOfExpr
class	InterfaceDecl
class	JavafePrimitiveType Represents a Java Front End PrimitiveType syntactic unit.
class	LabelStmt
class	LexicalPragma
class	LiteralExpr Represents a Literal.
class	LocalVarDecl Represents a LocalVariableDeclarationStatement.
class	MethodDecl
class	MethodInvocation Represents a MethodInvocation.
class	ModifierPragma
class	Name Treated as an immutable type.
class	NewArrayExpr
class	NewInstanceExpr
class	ObjectDesignator Designates the object or type used for a field or method access.
class	OnDemandImportDecl
class	ParenExpr
class	PrimitiveType Represents a PrimitiveType syntactic unit.
class	ReturnStmt
class	RoutineDecl Represents both MethodDeclarations and ConstructorDeclarations.
class	SimpleName
class	SingleTypeImportDecl
class	SkipStmt
class	Stmt Represents a BlockStatement syntactic unit (which includes variable declarations).
class	StmtPragma
class	SuperObjectDesignator Represents a ObjectDesignator of the form "super . ".
class	SwitchLabel Represents a SwitchLabel syntactic unit.
class	SwitchStmt
class	SynchronizeStmt
class	ThisExpr We represent [C.]this.
class	ThrowStmt
class	TryCatchStmt Represents a try-catch statement.
class	TryFinallyStmt
class	Type Represents a Type syntactic unit.
class	TypeDecl Represents a TypeDeclaration.
class	TypeDeclElemPragma
class	TypeModifierPragma
class	TypeName
class	TypeObjectDesignator Represents a ObjectDesignator of the form "TypeName . " Is created from AmbiguousVariableAccess/AmbiguousMethodInvocation by the name resolution code.
class	UnaryExpr Represents various kinds of unary expressions.
class	VarDeclStmt
class	VariableAccess Represents a simple name that is bound to a local variable declaration.
class	VarInit Represents a VariableInitializer.
class	WhileStmt

Methods in javafe.ast with parameters of type ASTNode

abstract java.lang.Object	VisitorArgResult.visitASTNode(ASTNode x, java.lang.Object o)
abstract void	Visitor.visitASTNode(ASTNode x)
static int	Util.size(ASTNode n) Returns the size of the AST n.
static int	Util.size(ASTNode n, int limit) Returns the size of the AST n (see above), except returns -1 if the size exceeds limit.
java.lang.String	StandardPrettyPrint.unknownTag(ASTNode n) Generate text to describe a ASTNote with an unknown tag
void	RShiftVisitor.visitASTNode(ASTNode x)
void	LShiftVisitor.visitASTNode(ASTNode x)
void	DefaultVisitor.visitASTNode(ASTNode x)
private void	ASTDotVisitor.writeDot(ASTNode parent, ASTNode current) recurses through the tree and writes the dotfile representation of it. if parent is null this is the root of the tree. current is the node we are parsing.
void	ASTDotVisitor.visitASTNode(ASTNode x) visits an ast node and outputs it in dot file format
java.lang.Object	ASTDecoration.get(ASTNode n) Return the decoration value of an ASTNode, or null if the ASTNode has no decoration.
void	ASTDecoration.set(ASTNode n, java.lang.Object val) Set the decoration value of an ASTNode.
java.lang.String	ASTDecoration.toString(ASTNode n) Return a string containing the decoration's name, and the decoration value for this ASTNode.

Uses of ASTNode in javafe.parser

Methods in javafe.parser that return ASTNode

static ASTNode	ParseUtil.setUniverse(ASTNode i, int u)
static ASTNode	ParseUtil.setUniverse(ASTNode i, int[] a, Type t, int loc)
static ASTNode	ParseUtil.setUniverse(GenericVarDecl i, int[] a)
static ASTNode	ParseUtil.setElementUniverse(ASTNode i, int u)

Methods in javafe.parser with parameters of type ASTNode

static ASTNode	ParseUtil.setUniverse(ASTNode i, int u)
static ASTNode	ParseUtil.setUniverse(ASTNode i, int[] a, Type t, int loc)
static int	ParseUtil.getUniverse(ASTNode i)
static ASTNode	ParseUtil.setElementUniverse(ASTNode i, int u)
static int	ParseUtil.getElementUniverse(ASTNode i)

Uses of ASTNode in javafe.tc

Subclasses of ASTNode in javafe.tc

class

TypeSig A TypeSig is a proxy and adaptor for TypeDecl.

Methods in javafe.tc that return ASTNode

ASTNode	EnvForTypeSig.locateFieldOrLocal(Identifier id) Locate the lexically innermost field or local variable declaration.
ASTNode	EnvForLocalType.locateFieldOrLocal(Identifier id) Locate the lexically innermost field or local variable declaration.
ASTNode	EnvForLocals.locateFieldOrLocal(Identifier id) Locate the lexically innermost field or local variable declaration.
ASTNode	EnvForEnclosedScope.locateFieldOrLocal(Identifier id) Locate the lexically innermost field or local variable declaration.
ASTNode	EnvForCU.locateFieldOrLocal(Identifier id) Locate the lexically innermost field or local variable declaration.
abstract ASTNode	Env.locateFieldOrLocal(Identifier id) Locate the lexically innermost field or local variable declaration with a given name.

Methods in javafe.tc with parameters of type ASTNode

static void	FlowInsensitiveChecks.checkUniverseAssignability(ASTNode l, ASTNode r) Tests if universe modifiers of r can be assigned to l.
static void	FlowInsensitiveChecks.checkUniverseCastability(ASTNode l, ASTNode r) Tests if the cast of the universe modifiers l r is ever possible.
protected Env	FlowInsensitiveChecks.checkModifierPragmaVec(ModifierPragmaVec v, ASTNode ctxt, Env env) Hook to do additional processing on ModifierVecs.
protected Env	FlowInsensitiveChecks.checkModifierPragma(ModifierPragma p, ASTNode ctxt, Env env) Hook to do additional processing on Modifiers.
protected Env	FlowInsensitiveChecks.checkTypeModifierPragmaVec(TypeModifierPragmaVec v, ASTNode ctxt, Env env)
protected Env	FlowInsensitiveChecks.checkTypeModifierPragma(TypeModifierPragma p, ASTNode ctxt, Env env)
protected static int	FlowInsensitiveChecks.universeTypeCombiner(ASTNode left, ASTNode right)
protected void	FlowInsensitiveChecks.checkNoRepInStaticContext(ASTNode n)
static void	FlowInsensitiveChecks.copyUniverses(ASTNode dest, ASTNode source)