|
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 CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectjavafe.tc.FlowInsensitiveChecks
escjava.tc.FlowInsensitiveChecks
Field Summary | |
protected static int |
ACC_LOW_BOUND_Package
|
protected static int |
ACC_LOW_BOUND_Private
|
protected static int |
ACC_LOW_BOUND_Protected
|
protected static int |
ACC_LOW_BOUND_Public
|
protected ASTNode |
accessibilityContext
If accessibilityLowerBound ! |
protected int |
accessibilityLowerBound
|
AnnotationHandler |
annotationHandler
|
protected int |
countFreeVarsAccesses
Counts the number of accesses of free variables and fields used for checking the appropriateness of invariants. |
static ASTDecoration |
envDecoration
|
static boolean |
inAnnotation
Are we in the middle of processing an annotation? |
static boolean |
inModelBody
|
protected boolean |
invariantContext
Indicates whether we are are checking an invariant pragma. |
protected boolean |
isInsidePRE
Indicates whether checking is currently being done inside a PRE .
|
protected boolean |
isLocksetContext
Indicates whether LS is allowed in this context. |
protected boolean |
isPredicateContext
Indicates whether a quantification or labeled predicate is allowed in this context. |
protected boolean |
isPrivateFieldAccessAllowed
Indicates whether private field accesses are allowed in the current context. |
protected boolean |
isRESContext
\result is allowed in this context when isRESContext
is true and returnType ! |
protected boolean |
isSpecDesignatorContext
Acts as a parameter to checkExpr . |
protected boolean |
isTwoStateContext
Indicates whether \old and \fresh are allowed in
this context. |
protected ExprStmtPragmaVec |
loopDecreases
Contains the loop decreases statement pragmas seen so far and not yet processed. |
protected ExprStmtPragmaVec |
loopInvariants
Contains the loop invariant statement pragmas seen so far and not yet processed. |
protected ExprStmtPragmaVec |
loopPredicates
|
static int |
MSTATUS_CLASS_NEW_METHOD
|
static int |
MSTATUS_NEW_ROUTINE
|
static int |
MSTATUS_OVERRIDE
|
protected LocalVarDeclVec |
skolemConstants
|
static ASTDecoration |
staticenvDecoration
|
Fields inherited from class javafe.tc.FlowInsensitiveChecks |
allowedExceptions, dontAddImplicitConstructorInvocations, enclosingLabels, inst, leftToRight, returnType, rootIEnv, rootSEnv, sig |
Constructor Summary | |
FlowInsensitiveChecks()
|
Method Summary | |
protected boolean |
assignmentConvertable(Expr e,
Type t)
Checks if Exp e can be assigned to Type t. |
protected Expr |
checkExpr(Env env,
Expr e)
This method should call setType on x before its
done. |
protected void |
checkLoopDecreases(Env env,
boolean allowed)
|
protected void |
checkLoopInvariants(Env env,
boolean allowed)
|
protected void |
checkLoopPredicates(Env env,
boolean allowed)
|
protected Env |
checkModifierPragma(ModifierPragma p,
ASTNode ctxt,
Env env)
Hook to do additional processing on Modifier s. |
protected Expr |
checkPredicate(Env env,
Expr e)
|
protected Env |
checkSkolemConstants(Env env,
boolean allowed)
|
protected Env |
checkStmt(Env env,
Stmt s)
Typecheck a statement in a given environment then return the environment in effect for statements that follow the given statement. |
protected Env |
checkStmtPragma(Env e,
StmtPragma s)
|
void |
checkTypeDeclaration(TypeSig s)
Moves s into implementation checked state. |
protected void |
checkTypeDeclElem(TypeDeclElem e)
|
protected void |
checkTypeDeclElemPragma(TypeDeclElemPragma e)
|
static void |
copyType(VarInit from,
VarInit to)
Copy the Type associated with an expression by the typechecking pass to another Expr. |
private void |
errorExpectingLoop(int loc,
int tag)
|
protected int |
getAccessibility(int modifiers)
|
static Set |
getAllOverrides(MethodDecl md)
|
static Set |
getDirectOverrides(MethodDecl md)
|
static int |
getOverrideStatus(RoutineDecl rd)
|
static MethodDecl |
getSuperClassOverride(MethodDecl md)
|
static MethodDecl |
getSuperNonNullStatus(RoutineDecl rd,
int j)
|
static MethodDecl |
getSuperNonNullStatus(RoutineDecl rd,
int j,
Set directOverrides)
|
static FlowInsensitiveChecks |
inst()
|
int |
isGhost(Expr t)
Returns non-zero if the expression is a ghost expression - that is, it would not exist if all ghost declarations were removed. |
int |
isGhost(ObjectDesignator od)
|
static boolean |
isMethodOverride(RoutineDecl rd)
|
static boolean |
isOverridable(MethodDecl md)
|
protected EnvForTypeSig |
makeEnvForTypeSig(TypeSig s,
boolean staticContext)
Override so that we use GhostEnv instead of EnvForTypeSig . |
Methods inherited from class javafe.tc.FlowInsensitiveChecks |
checkBinaryExpr, checkDesignator, checkExpr, checkExprVec, checkFieldDecl, checkForLoopAfterInit, checkInit, checkModifierPragmaVec, checkObjectDesignator, checkStmtVec, checkTypeModifierPragma, checkTypeModifierPragmaVec, checkTypeModifiers, getType, getTypeOrNull, reportLookupException, setType |
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
public static boolean inAnnotation
GhostEnv
.)
public static boolean inModelBody
public AnnotationHandler annotationHandler
protected boolean isLocksetContext
LS
is allowed in this context. The default is
true
. For contexts where LS
is not allowed,
isLocksetContext
should be set false
only temporarily.
protected boolean isRESContext
\result
is allowed in this context when isRESContext
is true
and returnType != null
. The default value
of isRESContext
is false
. For contexts where
isRESContext
should be true
,
isRESContext
should be set to true
only temporarily.
protected boolean isTwoStateContext
\old
and \fresh
are allowed in
this context. The default is false
. For contexts where these
functions are allowed, isTwoStateContext
should be set
true
only temporarily.
protected boolean isInsidePRE
PRE
.
This is used by the code that disallows nested PRE
expressions.
Note: alternatively, one could use isTwoStateContext
to implement
this functionality, but by having a separate bit, a more precise error message
can be produced.
protected boolean isPredicateContext
checkExpr
to a following recursive call.
protected boolean isPrivateFieldAccessAllowed
protected int accessibilityLowerBound
protected static final int ACC_LOW_BOUND_Private
protected static final int ACC_LOW_BOUND_Package
protected static final int ACC_LOW_BOUND_Protected
protected static final int ACC_LOW_BOUND_Public
protected ASTNode accessibilityContext
accessibilityLowerBound != ACC_LOW_BOUND_Private
, then
accessibilityContext
is the field or routine whose modifier
pragma is being type checked.
protected boolean isSpecDesignatorContext
checkExpr
. Its value is meaningful only
on entry to checkExpr
. It indicates whether the expression to be
checked is in a specification designator context. In particular, this
parameter is used to disallow array index wild cards in non-spec designator
contexts.
protected ExprStmtPragmaVec loopInvariants
protected ExprStmtPragmaVec loopDecreases
protected ExprStmtPragmaVec loopPredicates
protected LocalVarDeclVec skolemConstants
protected boolean invariantContext
protected int countFreeVarsAccesses
public static ASTDecoration envDecoration
public static ASTDecoration staticenvDecoration
public static final int MSTATUS_NEW_ROUTINE
public static final int MSTATUS_CLASS_NEW_METHOD
public static final int MSTATUS_OVERRIDE
Constructor Detail |
public FlowInsensitiveChecks()
Method Detail |
public static FlowInsensitiveChecks inst()
protected EnvForTypeSig makeEnvForTypeSig(TypeSig s, boolean staticContext)
GhostEnv
instead of EnvForTypeSig
.
makeEnvForTypeSig
in class FlowInsensitiveChecks
public void checkTypeDeclaration(TypeSig s)
FlowInsensitiveChecks
s
into implementation checked state.
checkTypeDeclaration
in class FlowInsensitiveChecks
protected void checkTypeDeclElem(TypeDeclElem e)
checkTypeDeclElem
in class FlowInsensitiveChecks
protected Env checkStmt(Env env, Stmt s)
FlowInsensitiveChecks
(The returned environment will be the same as the one passed in unless the statement is a declaration.)
checkStmt
in class FlowInsensitiveChecks
protected void checkLoopInvariants(Env env, boolean allowed)
protected void checkLoopDecreases(Env env, boolean allowed)
protected void checkLoopPredicates(Env env, boolean allowed)
protected Env checkSkolemConstants(Env env, boolean allowed)
private void errorExpectingLoop(int loc, int tag)
protected Expr checkPredicate(Env env, Expr e)
protected Expr checkExpr(Env env, Expr e)
FlowInsensitiveChecks
setType
on x
before its
done.
checkExpr
in class FlowInsensitiveChecks
protected void checkTypeDeclElemPragma(TypeDeclElemPragma e)
checkTypeDeclElemPragma
in class FlowInsensitiveChecks
protected Env checkModifierPragma(ModifierPragma p, ASTNode ctxt, Env env)
FlowInsensitiveChecks
Modifier
s. The
ASTNode
is the parent of the ModifierPragma
, and
env
is the current environment.
checkModifierPragma
in class FlowInsensitiveChecks
public static boolean isOverridable(MethodDecl md)
md
can be overridden in some possible
subclass.protected int getAccessibility(int modifiers)
accessibilityLowerBound
, given member modifiers.protected Env checkStmtPragma(Env e, StmtPragma s)
checkStmtPragma
in class FlowInsensitiveChecks
public static void copyType(VarInit from, VarInit to)
public static Set getAllOverrides(MethodDecl md)
public static Set getDirectOverrides(MethodDecl md)
public static MethodDecl getSuperClassOverride(MethodDecl md)
md
is a method that overrides a method in a
superclass, the overridden method is returned. Otherwise, if md
overrides a method in an interface, such a method is returned. Otherwise,
null
is returned.public static boolean isMethodOverride(RoutineDecl rd)
rd
is a method override declaration, that
is, whether or not rd
overrides a method declared in a superclass
or superinterface.public static int getOverrideStatus(RoutineDecl rd)
MSTATUS_NEW_ROUTINE
if rd
is a routine that
doesn't override any other method. This includes the case where
rd
is a constructor or a static method.
Returns MSTATUS_CLASS_NEW_METHOD
if rd
is a
method declared in a class, doesn't override any method in any superclass, but
overrides a method in an interface.
Otherwise, returns MSTATUS_OVERRIDE
.
public static MethodDecl getSuperNonNullStatus(RoutineDecl rd, int j)
public static MethodDecl getSuperNonNullStatus(RoutineDecl rd, int j, Set directOverrides)
public int isGhost(Expr t)
public int isGhost(ObjectDesignator od)
protected boolean assignmentConvertable(Expr e, Type t)
FlowInsensitiveChecks
Types
, because it needs to mess with constants.
assignmentConvertable
in class FlowInsensitiveChecks
|
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 CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |