|
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 VarInit | |
escjava | |
escjava.ast | |
escjava.backpred | |
escjava.parser | |
escjava.tc | |
escjava.translate | |
javafe.ast | |
javafe.parser | |
javafe.tc |
Uses of VarInit in escjava |
Subclasses of VarInit in escjava | |
static class |
AnnotationHandler.NonNullExpr
|
Uses of VarInit in escjava.ast |
Subclasses of VarInit in escjava.ast | |
class |
ArrayRangeRefExpr
|
class |
DefPredApplExpr
|
class |
DefPredLetExpr
|
class |
EverythingExpr
|
class |
GCExpr
|
class |
GeneralizedQuantifiedExpr
|
class |
GuardExpr
|
class |
LabelExpr
|
class |
LockSetExpr
|
class |
NaryExpr
|
class |
NothingExpr
|
class |
NotModifiedExpr
|
class |
NotSpecifiedExpr
|
class |
NumericalQuantifiedExpr
|
class |
QuantifiedExpr
|
class |
ResExpr
|
class |
SetCompExpr
|
class |
SubstExpr
|
class |
TypeExpr
|
class |
WildRefExpr
|
Methods in escjava.ast with parameters of type VarInit | |
void |
EscPrettyPrint.print(java.io.OutputStream o,
int ind,
VarInit e)
|
Uses of VarInit in escjava.backpred |
Methods in escjava.backpred with parameters of type VarInit | |
private static void |
BackPred.genFinalInitInfo(VarInit initExpr,
GenericVarDecl sDecl,
Expr s,
Expr x,
Type type,
int loc,
java.io.PrintStream proverStream)
|
protected static boolean |
BackPred.isStaticallyNonNull(VarInit e)
Do we know statically that an expression always returns a non-null value? |
Uses of VarInit in escjava.parser |
Methods in escjava.parser with parameters of type VarInit | |
static OldVarDecl |
OldVarDecl.make(Identifier id,
Type type,
int locId,
VarInit init,
int locAssignOp)
|
Uses of VarInit in escjava.tc |
Methods in escjava.tc with parameters of type VarInit | |
static void |
FlowInsensitiveChecks.copyType(VarInit from,
VarInit to)
Copy the Type associated with an expression by the typechecking pass to another Expr. |
Uses of VarInit in escjava.translate |
Methods in escjava.translate that return VarInit | |
private VarInit |
Translate.trim(VarInit E)
Peels off parentheses and casts from E and returns the result |
Methods in escjava.translate with parameters of type VarInit | |
private Expr |
Translate.ptrExpr(VarInit expr)
Purify and translate expr without protection |
private Expr |
Translate.trExpr(boolean protect,
VarInit expr)
Translate expr into a sequence of guarded commands that are
appended to code and return an expression denoting the value of
the expression. |
private void |
Translate.nullCheck(VarInit E,
Expr e,
int loc)
Emit a check at location loc that guarded command expression
e , which was translated from the Java expression E ,
is not null . |
private void |
Translate.nullCheck(VarInit E,
Expr e,
int loc,
int errorName,
int locPragma)
|
private VarInit |
Translate.trim(VarInit E)
Peels off parentheses and casts from E and returns the result |
private void |
Translate.writeCheck(Expr va,
VarInit Rval,
Expr rval,
int locAssignOp,
boolean inInitializerContext)
Insert checks done before writing variables, as prescribed by WriteCheck in ESCJ 16. |
private VariableAccess |
Translate.fresh(VarInit e,
int loc)
Generate a temporary for the result of a given expression. |
private VariableAccess |
Translate.fresh(VarInit e,
int loc,
java.lang.String suffix)
|
Expr |
Translate.addNewString(VarInit x,
Expr left,
Expr right)
|
private static java.lang.String |
Suggestion.gNull(VarInit E,
RoutineDecl rd)
|
private static java.lang.String |
Suggestion.gNeg(VarInit E,
RoutineDecl rd,
Set directTargets)
|
private static java.lang.String |
Suggestion.gArrStore(VarInit E,
RoutineDecl rd)
|
static boolean |
Purity.impure(VarInit expr)
Return true iff expr or any of its subexpressions
mutates the heap or local variables. |
static boolean |
Purity.pure(VarInit expr)
Return true iff neither expr nor any of its
subexpressions mutate the heap or local variables. |
private static void |
Purity.makeImpure(VarInit expr)
Set the decoration indicating the expr is
impure. |
static void |
Purity.decorate(VarInit expr)
Decorate expr and its subexpressions with purity
information. |
Uses of VarInit in javafe.ast |
Subclasses of VarInit 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 |
BinaryExpr
Represents various kinds of binary expressions (eg +,-,|,%=, etc). |
class |
CastExpr
|
class |
ClassLiteral
Represents a class literal (Type . class) |
class |
CondExpr
|
class |
Expr
Represents an Expression. |
class |
FieldAccess
Represents various kinds of field access expressions. |
class |
InstanceOfExpr
|
class |
LiteralExpr
Represents a Literal. |
class |
MethodInvocation
Represents a MethodInvocation. |
class |
NewArrayExpr
|
class |
NewInstanceExpr
|
class |
ParenExpr
|
class |
ThisExpr
We represent [C.]this. |
class |
UnaryExpr
Represents various kinds of unary expressions. |
class |
VariableAccess
Represents a simple name that is bound to a local variable declaration. |
Fields in javafe.ast declared as VarInit | |
private VarInit[] |
VarInitVec.elements
* Instance fields: * * |
VarInit |
LocalVarDecl.init
|
VarInit |
FieldDecl.init
|
Methods in javafe.ast that return VarInit | |
VarInit |
VarInitVec.elementAt(int index)
* Other methods: * * |
VarInit[] |
VarInitVec.toArray()
|
VarInit |
VarInitVec.pop()
|
Methods in javafe.ast with parameters of type VarInit | |
java.lang.Object |
VisitorArgResult.visitVarInit(VarInit x,
java.lang.Object o)
|
void |
Visitor.visitVarInit(VarInit x)
|
static VarInitVec |
VarInitVec.make(VarInit[] els)
|
void |
VarInitVec.setElementAt(VarInit x,
int index)
|
boolean |
VarInitVec.contains(VarInit x)
|
void |
VarInitVec.addElement(VarInit x)
|
boolean |
VarInitVec.removeElement(VarInit x)
|
void |
VarInitVec.insertElementAt(VarInit obj,
int index)
|
static void |
StandardPrettyPrint.println(VarInit e)
|
void |
StandardPrettyPrint.print(java.io.OutputStream o,
int ind,
VarInit e)
|
abstract void |
PrettyPrint.print(java.io.OutputStream o,
int ind,
VarInit e)
|
java.lang.String |
PrettyPrint.toString(VarInit e)
|
static LocalVarDecl |
LocalVarDecl.make(int modifiers,
ModifierPragmaVec pmodifiers,
Identifier id,
Type type,
int locId,
VarInit init,
int locAssignOp)
|
static FieldDecl |
FieldDecl.make(int modifiers,
ModifierPragmaVec pmodifiers,
Identifier id,
Type type,
int locId,
VarInit init,
int locAssignOp)
|
void |
DelegatingPrettyPrint.print(java.io.OutputStream o,
int ind,
VarInit e)
|
Constructors in javafe.ast with parameters of type VarInit | |
VarInitVec(VarInit[] els)
* Private constructors: * * |
Uses of VarInit in javafe.parser |
Methods in javafe.parser that return VarInit | |
VarInit |
ParseExpr.parseVariableInitializer(Lex l,
boolean specOnly)
Parse VariableInitializer. |
Uses of VarInit in javafe.tc |
Methods in javafe.tc that return VarInit | |
protected VarInit |
FlowInsensitiveChecks.checkInit(Env env,
VarInit x,
Type expectedResult)
|
static VarInit |
FlowInsensitiveChecks.setType(VarInit i,
Type t)
|
Methods in javafe.tc with parameters of type VarInit | |
void |
TypePrint.print(java.io.OutputStream o,
int ind,
VarInit e)
|
Type |
TypeCheck.getType(VarInit e)
Retrieves the Type of a VarInit . |
protected VarInit |
FlowInsensitiveChecks.checkInit(Env env,
VarInit x,
Type expectedResult)
|
static VarInit |
FlowInsensitiveChecks.setType(VarInit i,
Type t)
|
protected static Type |
FlowInsensitiveChecks.getTypeOrNull(VarInit i)
Retrieves the Type of a VarInit . |
static Type |
FlowInsensitiveChecks.getType(VarInit i)
Retrieves the Type of a VarInit . |
static void |
CheckInvariants.checkExpr(TypeSig sig,
VarInit expr)
|
|
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 |