|
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.Objectescjava.translate.TrAnExpr
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 |
private static int newStringCount
public static Translate translate
public static int level
public static int maxLevel
public static boolean extraSpecs
public static ExprVec trSpecExprAuxConditions
public static ExprVec trSpecExprAuxAssumptions
public static java.util.Map trSpecModelVarsUsed
public static java.util.Set trSpecAuxAxiomsNeeded
public static int tempn
public static java.util.LinkedList declStack
public static VariableAccess currentAlloc
public static VariableAccess currentState
public static java.util.LinkedList boundStack
protected static Expr specialResultExpr
TrSpecExpr
described in ESCJ 16. Each of the parameters sp
and st
is allowed to be null, which is interpreted
as the empty map.
protected static Expr specialThisExpr
protected static TrAnExpr inst
private static final int[][] binary_table
private static final int[][] unary_table
private static int cSubstReplacements
Constructor Detail |
public TrAnExpr()
Method Detail |
public static Expr trSpecExpr(Expr e)
TrSpecExpr
described in ESCJ 16. It is a shorthand for the full form in which
sp
and st
are passed in as empty maps.
public static Expr trSpecExpr(Expr e, Expr thisExpr)
public static void initForClause(boolean b)
public static void initForClause()
public static void closeForClause()
public static void initForRoutine()
public static boolean doRewrites()
public static Expr trSpecExpr(Expr e, java.util.Hashtable sp, java.util.Hashtable st, Expr thisExpr)
public static Expr trSpecExpr(Expr e, java.util.Hashtable sp, java.util.Hashtable st)
public Expr trSpecExprI(Expr e, java.util.Hashtable sp, java.util.Hashtable st)
static VariableAccess tempName(int loc, java.lang.String prefix, Type type)
public static java.util.Hashtable union(java.util.Hashtable h0, java.util.Hashtable h1)
public static Expr targetTypeCorrect(GenericVarDecl vd, java.util.Hashtable wt)
TargetTypeCorrect
,
except for the init$
case!
public static Expr typeCorrect(GenericVarDecl vd)
TypeCorrect
.
public static Expr typeCorrect(GenericVarDecl vd, java.util.Hashtable sp)
public static Expr quantTypeCorrect(GenericVarDecl vd, java.util.Hashtable sp)
public static Expr resultEqualsCall(GenericVarDecl vd, RoutineDecl rd, java.util.Hashtable sp)
public static Expr typeCorrectAs(GenericVarDecl vd, Type type)
public static Expr typeAndNonNullCorrectAs(GenericVarDecl vd, Type type, SimpleModifierPragma nonNullPragma, boolean forceNonNull, java.util.Hashtable sp)
public static ExprVec typeAndNonNullAllocCorrectAs(GenericVarDecl vd, Type type, SimpleModifierPragma nonNullPragma, boolean forceNonNull, java.util.Hashtable sp, boolean mentionAllocated)
public static Expr fieldTypeCorrect(FieldDecl fdecl)
public static Expr elemsTypeCorrect(GenericVarDecl edecl)
public static int getGCTagForBinary(BinaryExpr be)
public static int getGCTagForUnary(UnaryExpr e)
public static VariableAccess makeVarAccess(GenericVarDecl decl, int loc)
public static int getReplacementCount()
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.
protected static VariableAccess apply(java.util.Hashtable map, VariableAccess va)
public static TypeExpr trType(Type type)
public static void getCalledSpecs(RoutineDecl decl, ObjectDesignator od, ExprVec ev, Expr resultVar, java.util.Hashtable sp, java.util.Hashtable st)
public static Identifier fullName(RoutineDecl rd, boolean useSuper)
public static Expr getEquivalentAxioms(RepHelper o, java.util.Hashtable sp)
private static java.util.ArrayList makeBounds(RoutineDecl rd, GenericVarDecl newThis)
private static Expr createFunctionCall(RoutineDecl rd, java.util.ArrayList bounds, java.util.Hashtable sp)
private static Expr createForall(Expr expr, Expr fcall, java.util.ArrayList bounds)
public static Expr getRepresentsAxiom(NamedExprDeclPragma p, java.util.Hashtable sp)
public static Identifier representsMethodName(java.lang.Object pt)
public static ExprVec getModelVarAxioms(TypeDecl td, FieldDecl fd, java.util.Hashtable sp)
public static VariableAccess stateVar(java.util.Hashtable sp)
|
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 |