Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| 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

## escjava.tc
Class FlowInsensitiveChecks

    java.lang.Object
      javafe.tc.FlowInsensitiveChecks
          escjava.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 `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

### 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 `Modifier`s. 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`

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| 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

The ESC/Java2 Project Homepage