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

escjava.tc
Class FlowInsensitiveChecks

java.lang.Object
  extended byjavafe.tc.FlowInsensitiveChecks
      extended byescjava.tc.FlowInsensitiveChecks

public class FlowInsensitiveChecks
extends 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 Modifiers.
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

inAnnotation

public static boolean inAnnotation
Are we in the middle of processing an annotation? (Used by GhostEnv.)


inModelBody

public static boolean inModelBody

annotationHandler

public AnnotationHandler annotationHandler

isLocksetContext

protected boolean isLocksetContext
Indicates whether LS is allowed in this context. The default is true. For contexts where LS is not allowed, isLocksetContext should be set false only temporarily.


isRESContext

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.


isTwoStateContext

protected boolean isTwoStateContext
Indicates whether \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.


isInsidePRE

protected boolean isInsidePRE
Indicates whether checking is currently being done inside a 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.


isPredicateContext

protected boolean isPredicateContext
Indicates whether a quantification or labeled predicate is allowed in this context. This boolean is used only between one call of checkExpr to a following recursive call.


isPrivateFieldAccessAllowed

protected boolean isPrivateFieldAccessAllowed
Indicates whether private field accesses are allowed in the current context. Private field accesses are allowed everywhere, except in postconditions of overridable methods.


accessibilityLowerBound

protected int accessibilityLowerBound

ACC_LOW_BOUND_Private

protected static final int ACC_LOW_BOUND_Private
See Also:
Constant Field Values

ACC_LOW_BOUND_Package

protected static final int ACC_LOW_BOUND_Package
See Also:
Constant Field Values

ACC_LOW_BOUND_Protected

protected static final int ACC_LOW_BOUND_Protected
See Also:
Constant Field Values

ACC_LOW_BOUND_Public

protected static final int ACC_LOW_BOUND_Public
See Also:
Constant Field Values

accessibilityContext

protected ASTNode accessibilityContext
If accessibilityLowerBound != ACC_LOW_BOUND_Private, then accessibilityContext is the field or routine whose modifier pragma is being type checked.


isSpecDesignatorContext

protected boolean isSpecDesignatorContext
Acts as a parameter to 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.


loopInvariants

protected ExprStmtPragmaVec loopInvariants
Contains the loop invariant statement pragmas seen so far and not yet processed.


loopDecreases

protected ExprStmtPragmaVec loopDecreases
Contains the loop decreases statement pragmas seen so far and not yet processed.


loopPredicates

protected ExprStmtPragmaVec loopPredicates

skolemConstants

protected LocalVarDeclVec skolemConstants

invariantContext

protected boolean invariantContext
Indicates whether we are are checking an invariant pragma.


countFreeVarsAccesses

protected int countFreeVarsAccesses
Counts the number of accesses of free variables and fields used for checking the appropriateness of invariants.


envDecoration

public static ASTDecoration envDecoration

staticenvDecoration

public static ASTDecoration staticenvDecoration

MSTATUS_NEW_ROUTINE

public static final int MSTATUS_NEW_ROUTINE
See Also:
Constant Field Values

MSTATUS_CLASS_NEW_METHOD

public static final int MSTATUS_CLASS_NEW_METHOD
See Also:
Constant Field Values

MSTATUS_OVERRIDE

public static final int MSTATUS_OVERRIDE
See Also:
Constant Field Values
Constructor Detail

FlowInsensitiveChecks

public FlowInsensitiveChecks()
Method Detail

inst

public static FlowInsensitiveChecks inst()

makeEnvForTypeSig

protected EnvForTypeSig makeEnvForTypeSig(TypeSig s,
                                          boolean staticContext)
Override so that we use GhostEnv instead of EnvForTypeSig.

Overrides:
makeEnvForTypeSig in class FlowInsensitiveChecks

checkTypeDeclaration

public void checkTypeDeclaration(TypeSig s)
Description copied from class: FlowInsensitiveChecks
Moves s into implementation checked state.

Overrides:
checkTypeDeclaration in class FlowInsensitiveChecks

checkTypeDeclElem

protected void checkTypeDeclElem(TypeDeclElem e)
Overrides:
checkTypeDeclElem in class FlowInsensitiveChecks

checkStmt

protected Env checkStmt(Env env,
                        Stmt s)
Description copied from class: FlowInsensitiveChecks
Typecheck a statement in a given environment then return the environment in effect for statements that follow the given statement.

(The returned environment will be the same as the one passed in unless the statement is a declaration.)

Overrides:
checkStmt in class FlowInsensitiveChecks

checkLoopInvariants

protected void checkLoopInvariants(Env env,
                                   boolean allowed)

checkLoopDecreases

protected void checkLoopDecreases(Env env,
                                  boolean allowed)

checkLoopPredicates

protected void checkLoopPredicates(Env env,
                                   boolean allowed)

checkSkolemConstants

protected Env checkSkolemConstants(Env env,
                                   boolean allowed)

errorExpectingLoop

private void errorExpectingLoop(int loc,
                                int tag)

checkPredicate

protected Expr checkPredicate(Env env,
                              Expr e)

checkExpr

protected Expr checkExpr(Env env,
                         Expr e)
Description copied from class: FlowInsensitiveChecks
This method should call setType on x before its done.

Overrides:
checkExpr in class FlowInsensitiveChecks

checkTypeDeclElemPragma

protected void checkTypeDeclElemPragma(TypeDeclElemPragma e)
Overrides:
checkTypeDeclElemPragma in class FlowInsensitiveChecks

checkModifierPragma

protected Env checkModifierPragma(ModifierPragma p,
                                  ASTNode ctxt,
                                  Env env)
Description copied from class: FlowInsensitiveChecks
Hook to do additional processing on Modifiers. The ASTNode is the parent of the ModifierPragma, and env is the current environment.

Overrides:
checkModifierPragma in class FlowInsensitiveChecks
Returns:
true if pragma should be deleted

isOverridable

public static boolean isOverridable(MethodDecl md)
Returns:
whether or not md can be overridden in some possible subclass.

getAccessibility

protected int getAccessibility(int modifiers)
Returns:
a value appropriate for assignment to accessibilityLowerBound, given member modifiers.

checkStmtPragma

protected Env checkStmtPragma(Env e,
                              StmtPragma s)
Overrides:
checkStmtPragma in class FlowInsensitiveChecks

copyType

public static void copyType(VarInit from,
                            VarInit to)
Copy the Type associated with an expression by the typechecking pass to another Expr. This is used by Substitute to ensure it returns an Expr of the same Type.


getAllOverrides

public static Set getAllOverrides(MethodDecl md)
Returns:
a set of *all* the methods a given method overrides. This includes transitivity.

getDirectOverrides

public static Set getDirectOverrides(MethodDecl md)

getSuperClassOverride

public static MethodDecl getSuperClassOverride(MethodDecl md)
Returns:
If 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.

isMethodOverride

public static boolean isMethodOverride(RoutineDecl rd)
Returns:
whether or not rd is a method override declaration, that is, whether or not rd overrides a method declared in a superclass or superinterface.

getOverrideStatus

public static int getOverrideStatus(RoutineDecl rd)
Returns:
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.


getSuperNonNullStatus

public static MethodDecl getSuperNonNullStatus(RoutineDecl rd,
                                               int j)
Returns:
null if method md is allowed to declare its jth (counting from 0) formal parameter as non_null. That is the case if the method does not override anything, or if in everything that it does override that parameter is declared non_null. Otherwise returns the MethodDecl corresponding to the overridden method with which the argument rd is in conflict.

getSuperNonNullStatus

public static MethodDecl getSuperNonNullStatus(RoutineDecl rd,
                                               int j,
                                               Set directOverrides)

isGhost

public 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. Otherwise returns a Location value of a relevant non-ghost declaration.


isGhost

public int isGhost(ObjectDesignator od)

assignmentConvertable

protected boolean assignmentConvertable(Expr e,
                                        Type t)
Description copied from class: FlowInsensitiveChecks
Checks if Exp e can be assigned to Type t. This method is here instead of in Types, because it needs to mess with constants.

Overrides:
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

The ESC/Java2 Project Homepage