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.translate
Class TrAnExpr

    java.lang.Object
      escjava.translate.TrAnExpr

public class TrAnExpr
extends java.lang.Object

Translates Annotation Expressions to GCExpr.

Field Summary
`private static int[][]` | `binary_table`
`static java.util.LinkedList` | `boundStack`
`private static int` | `cSubstReplacements`
`static VariableAccess` | `currentAlloc`
`static VariableAccess` | `currentState`
`static java.util.LinkedList` | `declStack`
`static boolean` | `extraSpecs`
`protected static TrAnExpr` | `inst`
`static int` | `level`
`static int` | `maxLevel`
`private static int` | `newStringCount` This hashtable keeps track of cautions issued, with respect to using variables in \old pragmas that were not mentioned in modifies pragmas.
`protected static Expr` | `specialResultExpr` This is the full form of function `TrSpecExpr` described in ESCJ 16.
`protected static Expr` | `specialThisExpr`
`static int` | `tempn`
`static Translate` | `translate`
`static java.util.Set` | `trSpecAuxAxiomsNeeded`
`static ExprVec` | `trSpecExprAuxAssumptions`
`static ExprVec` | `trSpecExprAuxConditions`
`static java.util.Map` | `trSpecModelVarsUsed`
`private static int[][]` | `unary_table`

Constructor Summary
`TrAnExpr()`

Method Summary
`protected static VariableAccess` | `apply(java.util.Hashtable map, VariableAccess va)`
`static void` | `closeForClause()`
`private static Expr` | `createForall(Expr expr, Expr fcall, java.util.ArrayList bounds)`
`private static Expr` | `createFunctionCall(RoutineDecl rd, java.util.ArrayList bounds, java.util.Hashtable sp)`
`static boolean` | `doRewrites()`
`static Expr` | `elemsTypeCorrect(GenericVarDecl edecl)`
`static Expr` | `fieldTypeCorrect(FieldDecl fdecl)`
`static Identifier` | `fullName(RoutineDecl rd, boolean useSuper)`
`static void` | `getCalledSpecs(RoutineDecl decl, ObjectDesignator od, ExprVec ev, Expr resultVar, java.util.Hashtable sp, java.util.Hashtable st)`
`static Expr` | `getEquivalentAxioms(RepHelper o, java.util.Hashtable sp)`
`static int` | `getGCTagForBinary(BinaryExpr be)`
`static int` | `getGCTagForUnary(UnaryExpr e)` TBW.
`static ExprVec` | `getModelVarAxioms(TypeDecl td, FieldDecl fd, java.util.Hashtable sp)`
`static int` | `getReplacementCount()` Returns the number of variable substitutions that calls to `trSpecExpr` have caused.
`static Expr` | `getRepresentsAxiom(NamedExprDeclPragma p, java.util.Hashtable sp)` Translates an individual represents clause into a class-level axiom.
`static void` | `initForClause()`
`static void` | `initForClause(boolean b)`
`static void` | `initForRoutine()`
`private static java.util.ArrayList` | `makeBounds(RoutineDecl rd, GenericVarDecl newThis)`
`static VariableAccess` | `makeVarAccess(GenericVarDecl decl, int loc)`
`static Expr` | `quantTypeCorrect(GenericVarDecl vd, java.util.Hashtable sp)`
`static Identifier` | `representsMethodName(java.lang.Object pt)`
`static Expr` | `resultEqualsCall(GenericVarDecl vd, RoutineDecl rd, java.util.Hashtable sp)`
`static VariableAccess` | `stateVar(java.util.Hashtable sp)`
`static Expr` | `targetTypeCorrect(GenericVarDecl vd, java.util.Hashtable wt)` This method implements the ESCJ 16 function `TargetTypeCorrect`, except for the `init$` case!
`(package private) static VariableAccess` | `tempName(int loc, java.lang.String prefix, Type type)`
`static Expr` | `trSpecExpr(Expr e)` This is the abbreviated form of function `TrSpecExpr` described in ESCJ 16.
`static Expr` | `trSpecExpr(Expr e, Expr thisExpr)`
`static Expr` | `trSpecExpr(Expr e, java.util.Hashtable sp, java.util.Hashtable st)`
`static Expr` | `trSpecExpr(Expr e, java.util.Hashtable sp, java.util.Hashtable st, Expr thisExpr)`
`Expr` | `trSpecExprI(Expr e, java.util.Hashtable sp, java.util.Hashtable st)`
`static TypeExpr` | `trType(Type type)`
`static ExprVec` | `typeAndNonNullAllocCorrectAs(GenericVarDecl vd, Type type, SimpleModifierPragma nonNullPragma, boolean forceNonNull, java.util.Hashtable sp, boolean mentionAllocated)` Returns a vector of conjuncts.
`static Expr` | `typeAndNonNullCorrectAs(GenericVarDecl vd, Type type, SimpleModifierPragma nonNullPragma, boolean forceNonNull, java.util.Hashtable sp)`
`static Expr` | `typeCorrect(GenericVarDecl vd)` This method implements the ESCJ 16 function `TypeCorrect`.
`static Expr` | `typeCorrect(GenericVarDecl vd, java.util.Hashtable sp)`
`static Expr` | `typeCorrectAs(GenericVarDecl vd, Type type)`
`static java.util.Hashtable` | `union(java.util.Hashtable h0, java.util.Hashtable h1)`

Methods inherited from class java.lang.Object
`clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

Field Detail

### newStringCount

    private static int newStringCount

  This hashtable keeps track of cautions issued, with respect to using variables in \old pragmas that were not mentioned in modifies pragmas. The purpose of this hashtable is to prevent issuing duplicate cautions.

### translate

    public static Translate translate

### level

    public static int level

### maxLevel

    public static int maxLevel

### extraSpecs

    public static boolean extraSpecs

### trSpecExprAuxConditions

    public static ExprVec trSpecExprAuxConditions

### trSpecExprAuxAssumptions

    public static ExprVec trSpecExprAuxAssumptions

### trSpecModelVarsUsed

    public static java.util.Map trSpecModelVarsUsed

### trSpecAuxAxiomsNeeded

    public static java.util.Set trSpecAuxAxiomsNeeded

### tempn

    public static int tempn

### declStack

    public static java.util.LinkedList declStack

### currentAlloc

    public static VariableAccess currentAlloc

### currentState

    public static VariableAccess currentState

### boundStack

    public static java.util.LinkedList boundStack

### specialResultExpr

    protected static Expr specialResultExpr

  This is the full form of function `TrSpecExpr` described in ESCJ 16. Each of the parameters `sp` and `st` is allowed to be null, which is interpreted as the empty map.

### specialThisExpr

    protected static Expr specialThisExpr

### inst

    protected static TrAnExpr inst

### binary_table

    private static final int[][] binary_table

### unary_table

    private static final int[][] unary_table

### cSubstReplacements

    private static int cSubstReplacements

Constructor Detail

### TrAnExpr

    public TrAnExpr()

Method Detail

### trSpecExpr

    public static Expr trSpecExpr(Expr e)

  This is the abbreviated form of function `TrSpecExpr` described in ESCJ 16. It is a shorthand for the full form in which `sp` and `st` are passed in as empty maps.

### trSpecExpr

    public static Expr trSpecExpr(Expr e,
                                  Expr thisExpr)

### initForClause

    public static void initForClause(boolean b)

### initForClause

    public static void initForClause()

### closeForClause

    public static void closeForClause()

### initForRoutine

    public static void initForRoutine()

### doRewrites

    public static boolean doRewrites()

### trSpecExpr

    public static Expr trSpecExpr(Expr e,
                                  java.util.Hashtable sp,
                                  java.util.Hashtable st,
                                  Expr thisExpr)

### trSpecExpr

    public static Expr trSpecExpr(Expr e,
                                  java.util.Hashtable sp,
                                  java.util.Hashtable st)

### trSpecExprI

    public Expr trSpecExprI(Expr e,
                            java.util.Hashtable sp,
                            java.util.Hashtable st)

### tempName

    static VariableAccess tempName(int loc,
                                   java.lang.String prefix,
                                   Type type)

### union

    public static java.util.Hashtable union(java.util.Hashtable h0,
                                            java.util.Hashtable h1)

### targetTypeCorrect

    public static Expr targetTypeCorrect(GenericVarDecl vd,
                                         java.util.Hashtable wt)

  This method implements the ESCJ 16 function `TargetTypeCorrect`, except for the `init$` case!

### typeCorrect

    public static Expr typeCorrect(GenericVarDecl vd)

  This method implements the ESCJ 16 function `TypeCorrect`.

### typeCorrect

    public static Expr typeCorrect(GenericVarDecl vd,
                                   java.util.Hashtable sp)

### quantTypeCorrect

    public static Expr quantTypeCorrect(GenericVarDecl vd,
                                        java.util.Hashtable sp)

### resultEqualsCall

    public static Expr resultEqualsCall(GenericVarDecl vd,
                                        RoutineDecl rd,
                                        java.util.Hashtable sp)

### typeCorrectAs

    public static Expr typeCorrectAs(GenericVarDecl vd,
                                     Type type)

### typeAndNonNullCorrectAs

    public static Expr typeAndNonNullCorrectAs(GenericVarDecl vd,
                                               Type type,
                                               SimpleModifierPragma nonNullPragma,
                                               boolean forceNonNull,
                                               java.util.Hashtable sp)

### typeAndNonNullAllocCorrectAs

    public static ExprVec typeAndNonNullAllocCorrectAs(GenericVarDecl vd,
                                                       Type type,
                                                       SimpleModifierPragma nonNullPragma,
                                                       boolean forceNonNull,
                                                       java.util.Hashtable sp,
                                                       boolean mentionAllocated)

  Returns a vector of conjuncts. This vector is "virgin" and can be modified by the caller. It contains at least 2 empty slots, allows clients to append a couple of items without incurring another allocation.

### fieldTypeCorrect

    public static Expr fieldTypeCorrect(FieldDecl fdecl)

### elemsTypeCorrect

    public static Expr elemsTypeCorrect(GenericVarDecl edecl)

### getGCTagForBinary

    public static int getGCTagForBinary(BinaryExpr be)

### getGCTagForUnary

    public static int getGCTagForUnary(UnaryExpr e)

  TBW. Requires e.getTag() in { UNARYSUB, NOT, BITNOT, INC, POSTFIXINC, DEC, POSTFIXDEC }

### makeVarAccess

    public static VariableAccess makeVarAccess(GenericVarDecl decl,
                                               int loc)

### getReplacementCount

    public static int getReplacementCount()

  Returns the number of variable substitutions that calls to `trSpecExpr` have caused. To find out how many times a substitution was made, a caller can surround the call to `trSpecExpr` by two calls to this method and compute the difference.

### apply

    protected static VariableAccess apply(java.util.Hashtable map,
                                          VariableAccess va)

### trType

    public static TypeExpr trType(Type type)

### getCalledSpecs

    public static void getCalledSpecs(RoutineDecl decl,
                                      ObjectDesignator od,
                                      ExprVec ev,
                                      Expr resultVar,
                                      java.util.Hashtable sp,
                                      java.util.Hashtable st)

### fullName

    public static Identifier fullName(RoutineDecl rd,
                                      boolean useSuper)

### getEquivalentAxioms

    public static Expr getEquivalentAxioms(RepHelper o,
                                           java.util.Hashtable sp)

### makeBounds

    private static java.util.ArrayList makeBounds(RoutineDecl rd,
                                                  GenericVarDecl newThis)

### createFunctionCall

    private static Expr createFunctionCall(RoutineDecl rd,
                                           java.util.ArrayList bounds,
                                           java.util.Hashtable sp)

### createForall

    private static Expr createForall(Expr expr,
                                     Expr fcall,
                                     java.util.ArrayList bounds)

### getRepresentsAxiom

    public static Expr getRepresentsAxiom(NamedExprDeclPragma p,
                                          java.util.Hashtable sp)

  Translates an individual represents clause into a class-level axiom.

### representsMethodName

    public static Identifier representsMethodName(java.lang.Object pt)

### getModelVarAxioms

    public static ExprVec getModelVarAxioms(TypeDecl td,
                                            FieldDecl fd,
                                            java.util.Hashtable sp)

### stateVar

    public static VariableAccess stateVar(java.util.Hashtable sp)

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