|
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.Translate
Nested Class Summary | |
class |
Translate.EverythingLoc
|
static class |
Translate.Strings
|
Field Summary | |
static java.util.Set |
axsToAdd
|
private Identifier |
cacheVar
|
private StackVector |
code
Contains the guarded commands generated so far for the current method. |
private GuardedCmdVec |
codevec
|
private StackVector |
declaredLocals
Contains the local Java variables declared in the current block so far for the current block and enclosing blocks of the current method. |
(package private) Frame |
frameHandler
|
private boolean |
inConstructorContext
Indicates whether or not the current routine is in a "constructor context", meaning that it is a constructor being checked or a method in the same class that's being inlined into the constructor. |
int |
inlineCheckDepth
|
static ASTDecoration |
inlineDecoration
Describes what aspects of an inlined call to check and what aspects to either assert or simply ignore. |
int |
inlineDepthPastCheck
|
private Translate |
inlineParent
Singly-linked list of the inline parents. |
private boolean |
issueCautions
Indicates whether to issue cautions. |
private java.util.ArrayList |
locList
|
private ExprStmtPragmaVec |
loopDecreases
List of loop decreases pragmas seen so far (and not yet used) within the current method. |
private ExprStmtPragmaVec |
loopinvariants
List of loop invariant pragmas seen so far (and not yet used) within the current method. |
private ExprStmtPragmaVec |
loopPredicates
|
java.util.ArrayList |
modifyEverythingLocations
|
private ExprVec |
mutexList
Used by readCheck and writeCheck to accumulate the
list of mutexes protecting a shared variable. |
private Set |
predictedSynTargs
Describes the current predicted set of synTargs. |
private java.util.Hashtable |
premap
|
private java.util.Hashtable |
premapWithArgs
|
private RoutineDecl |
rdCurrent
References the routine currently being checked by trBody. |
private FindContributors |
scope
Describes the current scope. |
protected LocalVarDeclVec |
skolemConstants
|
private StackVector |
temporaries
Contains the temporaries that generated for the current method that haven't yet been declared in a VARINCMD. |
private int |
tmpcount
Countains the number of temporaries generated for the method currently being translated. |
private TypeDecl |
typeDecl
The type containing the routine whose body is being translated. |
Constructor Summary | |
Translate()
|
Method Summary | |
private void |
addAssumption(Expr pred)
|
private void |
addAssumptions(ExprVec ev)
|
private void |
addCheck(ASTNode use,
int errorName,
Expr pred)
Calls GC.check to create a check and appends the result to
code . |
private void |
addCheck(int locUse,
Condition cond)
Calls GC.check to create a check and appends the result to
code . |
(package private) void |
addCheck(int locUse,
int errorName,
Expr pred)
Calls GC.check to create a check and appends the result to
code . |
private void |
addCheck(int locUse,
int errorName,
Expr pred,
ASTNode prag)
Calls GC.check to create a check and appends the
result to code . |
private void |
addCheck(int locUse,
int errorName,
Expr pred,
int locPragmaDecl)
Calls GC.check to create a check and appends the result to
code . |
(package private) void |
addCheck(int locUse,
int errorName,
Expr pred,
int locPragmaDecl,
int auxLoc)
|
private void |
addCheck(int locUse,
int errorName,
Expr pred,
int locPragmaDecl,
java.lang.Object aux)
Calls GC.check to create a check and appends the result to
code . |
private void |
addLoopDecreases(LoopCmd loop,
int piece)
Adds to code the various pieces of the translation of the
decreases pragma. |
void |
addMoreLocations(java.util.Set s)
|
private void |
addNewAssumptions()
|
private void |
addNewAssumptionsHelper()
|
(package private) ExprVec |
addNewAssumptionsNow()
|
private void |
addNewAssumptionsNow(ExprVec ev)
|
Expr |
addNewString(VarInit x,
Expr left,
Expr right)
|
private static Expr |
addRelAsgCast(Expr rval,
Type lType,
Type rType)
|
static void |
addTraceLabelSequenceNumbers(GuardedCmd gc)
Destructively change the trace labels in gc to insert sequence
numbers that are used by the ErrorMsg class in printing trace labels in the
correct execution order. |
private VariableAccess |
adorn(VariableAccess v)
Make a fresh version of a special variable to save it in. |
private void |
arrayAccessCheck(Expr Array,
Expr array,
Expr Index,
Expr index,
int locOpenBracket)
Emit the checks that array is non-null and that
index is inbounds for array . |
private Expr |
breakLabel(Stmt s)
|
VariableAccess |
cacheValue(Expr e)
|
private Call |
call(RoutineDecl rd,
ExprVec argsRaw,
ExprVec args,
FindContributors scope,
int scall,
int ecall,
int locOpenParen,
boolean superOrSiblingConstructorCall,
InlineSettings inline,
Expr eod,
boolean freshResult)
Creates and desugars a call node, extended to allow the possibility of inlining a call. |
private void |
checkLoopInvariants(LoopCmd loop,
ExprVec axs)
Add to "code" checks for all loop invariants of "loop". |
private GuardedCmd |
cloneGuardedCommand(GuardedCmd gc)
This method returns a guarded command G that is like
gc except that where gc contains a mutable command,
G contains a fresh copy of that command. |
private InlineSettings |
computeInlineSettings(RoutineDecl rd,
ExprVec argsRaw,
InlineSettings inline,
int scall)
Computes the inlining settings for a given call. |
private Expr |
continueLabel(Stmt s)
|
private void |
desugarLoopFast(LoopCmd loop,
ExprVec axs)
Desugars loop according to the fast option. |
void |
desugarLoopSafe(LoopCmd loop,
ExprVec axs)
Desugars loop according to the safe option. |
private VariableAccess |
fresh(VarInit e,
int loc)
Generate a temporary for the result of a given expression. |
private VariableAccess |
fresh(VarInit e,
int loc,
java.lang.String suffix)
|
private TypeExpr |
getClassObject(TypeDecl tdClass)
|
private static VariableAccess |
getInitVar(GenericVarDecl d)
Return the VariableAccesss associated with d by a
call to setInitVar . |
static void |
globallyTurnOffChecks(boolean flag)
If the flag is true, set all assertion checks to assumes. |
private void |
guard(Expr e,
Expr label)
Computes purity information for Java expression e , translates
e (emitting any code needed to account for impurities or side
effects in the expression), and emits code that performs a RAISE
label command if the expression evaluates to false . |
private VariableAccess |
initadorn(LocalVarDecl d)
Make a fresh "boolean" variable to hold the initialized status of a Java variable that is marked as "uninitialized". |
private java.util.Hashtable |
initializeRWCheckSubstMap(java.util.Hashtable prevMap,
Expr actualSelf,
int loc)
The following method is used in readCheck and writeCheck to lazily construct a substitution map (which may also create another temporary variable). |
private void |
instanceInitializers(TypeDecl tdecl)
This method implements "InstanceInitializers", as described in section 8.1 of ESCJ 16. |
private void |
instanceInitializeZero(TypeDecl tdecl)
Called by instanceInitializers . |
static boolean |
isFinal(Type t)
|
private boolean |
isRecursiveInvocation(RoutineDecl r)
|
private boolean |
isStandaloneConstructor(RoutineDecl rd)
|
private void |
makeLoop(int sLoop,
int eLoop,
int locHotspot,
GenericVarDeclVec tempVars,
GuardedCmd guard,
GuardedCmd body,
ExprStmtPragmaVec J,
ExprStmtPragmaVec decreases,
LocalVarDeclVec skolemConsts,
ExprStmtPragmaVec P,
Expr label)
Appends to code commands that make up a loop with nominal body
guard;body , where label is raised within
body to terminate the loop. |
static Expr |
mapLocation(Expr e,
int loc)
|
private GuardedCmd |
modify(Expr e,
java.util.Hashtable pt,
int loc)
|
GuardedCmd |
modify(Set simpleTargets,
int loc)
|
private GuardedCmd |
modify(VariableAccess va,
int loc)
Modifies a GC designator. |
GuardedCmd |
modifyATargets(Set aTargets,
int loc)
targets is set of GenericVarDecls. aTargets is set of ATargets. |
private void |
nullCheck(VarInit E,
Expr e,
int loc)
Emit a check at location loc that guarded command expression
e , which was translated from the Java expression E ,
is not null . |
private void |
nullCheck(VarInit E,
Expr e,
int loc,
int errorName,
int locPragma)
|
private GuardedCmd |
opBlockCmd(Expr label)
Reduces number of stack marks by 1. |
private static int |
orderTraceLabel(LabelExpr le,
int count)
If the given label is a trace label, add the count number to the
given label expression's label name, so that trace labels will sort correctly. |
private static int |
orderTraceLabels(GuardedCmd gc,
int count)
Walk through the guarded command translation of a method, adding unique number to its location sequence, in order to sort trace labels in order of execution. |
private GuardedCmd |
popDeclBlock()
Pops the code and declared local variables, makes these into a command (usually a VAR .. |
private static Expr |
predArrayOwnerNull(VariableAccess allocOld,
VariableAccess allocNew,
VariableAccess arr)
Returns the guarded-command expression: (FORALL o :: ! |
private static Expr |
predEvathangsAnArray(VariableAccess allocOld,
VariableAccess allocNew)
Returns the guarded-command expression: (FORALL o :: ! |
private Expr |
protect(boolean protect,
Expr e,
int loc)
Extends the code array with a command that evaluates e and returns an expession which denotes this value in the poststate of that command. |
private Expr |
protect(boolean protect,
Expr e,
int loc,
java.lang.String suffix)
|
private Expr |
ptrExpr(VarInit expr)
Purify and translate expr without protection |
private void |
raise(Expr label)
Emits the commands EC= label; raise to code . |
private void |
readCheck(Expr va,
int locId)
Insert checks done before reading variables. |
private static void |
setInitVar(GenericVarDecl d,
VariableAccess init)
Associates init with d ; will be returned by a call
to getInitVar . |
(package private) static void |
setop(ASTNode e)
|
private GuardedCmd |
spill()
Pops temporaries and code, and makes these into a VARINCMD command that is returned. |
private static GuardedCmd |
substituteGC(java.util.Hashtable pt,
GuardedCmd gc)
When a call is inlined, we need to substitute the new names given to its formal parameters for its original names in the inlined body. |
private VariableAccess |
temporary(java.lang.String s,
int locAccess)
Generate a temporary variable with prefix s and associated
expression location information locAccess . |
private VariableAccess |
temporary(java.lang.String s,
int locAccess,
int locIdDecl)
|
private GuardedCmd |
traceInfoLabelCmd(ASTNode ast,
java.lang.String traceInfoTag)
|
private GuardedCmd |
traceInfoLabelCmd(ASTNode ast,
java.lang.String traceInfoTag,
int loc)
|
private GuardedCmd |
traceInfoLabelCmd(int sloc,
int eloc,
java.lang.String traceInfoTag,
int loc)
|
private GuardedCmd |
traceInfoLabelCmd(int sloc,
int eloc,
java.lang.String traceInfoTag,
java.lang.String sortSeq)
|
GuardedCmd |
trBody(RoutineDecl rd,
FindContributors scope,
java.util.Hashtable premap,
Set predictedSynTargs,
Translate inlineParent,
boolean issueCautions)
Translates the body of a method or constructor, as described in ESCJ 16, section 8. |
private void |
trConstructorBody(ConstructorDecl cd,
java.util.Hashtable premap)
Auxiliary routine used by trBody to translate the body of a constructor, as described in ESCJ 16, section 8. |
private void |
trConstructorCallStmt(ConstructorInvocation ci)
This method implements "TrConstructorCallStmt" as described in section 6 of ESCJ 16. |
private Expr |
trExpr(boolean protect,
VarInit expr)
Translate expr into a sequence of guarded commands that are
appended to code and return an expression denoting the value of
the expression. |
private Expr |
trFieldAccess(boolean protectObject,
FieldAccess fa)
Returns either a VariableAccess if fa is a class
variable or a SELECT application if fa is an
instance variable access, or an ARRAYLENGTH application if
fa is the final array field length . |
private void |
trIfStmt(Expr guard,
Stmt thenStmt,
Stmt elseStmt,
TypeDecl decl)
Translate an "if" statement. |
private VarInit |
trim(VarInit E)
Peels off parentheses and casts from E and returns the result |
private Expr |
trMethodInvocation(boolean protect,
MethodInvocation mi)
This translation of method invocation follows section 4.1 of ESCJ 16. |
private void |
trStmt(Stmt stmt,
TypeDecl decl)
Translate stmt into a sequence of guarded commands
that are appended to code .
|
private void |
trSynchronizedBody(Expr mu,
Stmt stmt,
int loc,
TypeDecl decl)
|
private void |
wrapUpDeclBlock()
Pops declaredLocals and code and then appends
code with a VARINCMD (if there were any new declared locals) or a
sequence of commands (otherwise). |
private GuardedCmd |
wrapUpUnrolledIteration(java.lang.String locString,
int iteration,
GenericVarDeclVec tempVars)
|
private void |
writeCheck(Expr va,
VarInit Rval,
Expr rval,
int locAssignOp,
boolean inInitializerContext)
Insert checks done before writing variables, as prescribed by WriteCheck in ESCJ 16. |
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
Frame frameHandler
public static java.util.Set axsToAdd
private java.util.Hashtable premap
private java.util.Hashtable premapWithArgs
private TypeDecl typeDecl
private RoutineDecl rdCurrent
private Translate inlineParent
null
if this
translation is not being inlined.
private boolean issueCautions
private boolean inConstructorContext
private final StackVector code
code
gets pushed. As blocks
are left, code
is poped into a GuardedCmdVec
which
is wrapped inside a BLOCK guarded command that gets appended onto
code
.
private ExprStmtPragmaVec loopinvariants
private ExprStmtPragmaVec loopDecreases
private ExprStmtPragmaVec loopPredicates
protected LocalVarDeclVec skolemConstants
private final StackVector declaredLocals
code
: Each time a Java block
is entered, declaredLocals
gets pushed; when a block is left,
declaredLocals
is popped into a GenericVarDeclVec
that gets wrapped inside a BLOCK guarded command.
private final StackVector temporaries
private FindContributors scope
private Set predictedSynTargs
If non-null, then represents an *upper* bound on freeVars of the result of the current trBody(...) call.
public static final ASTDecoration inlineDecoration
InlineSettings
object in which the
nextInlineCheckDepth
and
nextInlineDepthPastCheck
fields are unused.
This variable is used only for some call-site specific
inlining, in particular, currently only to handle the
-inlineConstructors flag. Other reasons for inlining are taken
care of in method computeInlineSettings
.
private ExprVec mutexList
readCheck
and writeCheck
to accumulate the
list of mutexes protecting a shared variable. Thus, these methods are not
thread re-entrant.
private java.util.ArrayList locList
public int inlineCheckDepth
public int inlineDepthPastCheck
private int tmpcount
Reset to 0 on entry to trExpr(boolean, VarInit)
.
public java.util.ArrayList modifyEverythingLocations
private GuardedCmdVec codevec
private Identifier cacheVar
Constructor Detail |
public Translate()
Method Detail |
public GuardedCmd trBody(RoutineDecl rd, FindContributors scope, java.util.Hashtable premap, Set predictedSynTargs, Translate inlineParent, boolean issueCautions)
predictedSynTargs
- for correct translation, this must contain an upper
bound for the syntactic targets of the result of this call. A value of null is
taken to represent the set of all variables & is hence always a safe value.private boolean isStandaloneConstructor(RoutineDecl rd)
true
when rd
is a constructor that does not
call a sibling constructor.private void trConstructorBody(ConstructorDecl cd, java.util.Hashtable premap)
private TypeExpr getClassObject(TypeDecl tdClass)
private void instanceInitializers(TypeDecl tdecl)
private void instanceInitializeZero(TypeDecl tdecl)
instanceInitializers
.
private GuardedCmd spill()
private VariableAccess adorn(VariableAccess v)
private VariableAccess initadorn(LocalVarDecl d)
private boolean isRecursiveInvocation(RoutineDecl r)
private GuardedCmd opBlockCmd(Expr label)
private Expr breakLabel(Stmt s)
private Expr continueLabel(Stmt s)
private void raise(Expr label)
EC= label; raise
to code
.
private void guard(Expr e, Expr label)
e
, translates
e
(emitting any code needed to account for impurities or side
effects in the expression), and emits code that performs a RAISE
label
command if the expression evaluates to false
. As
usual, emitted code is appended to code
and temporaries are
appended to temporaries
.
private void makeLoop(int sLoop, int eLoop, int locHotspot, GenericVarDeclVec tempVars, GuardedCmd guard, GuardedCmd body, ExprStmtPragmaVec J, ExprStmtPragmaVec decreases, LocalVarDeclVec skolemConsts, ExprStmtPragmaVec P, Expr label)
code
commands that make up a loop with nominal body
guard;body
, where label
is raised within
body
to terminate the loop. The vector J
contains
the user-declared loop invariant pragmas. The vector decreases
contains the user-declared bound function pragmas. The scope of the variables
in tempVars
is the nominal body; this method will wrap an
appropriate var .. in .. end
command around these.
private void desugarLoopFast(LoopCmd loop, ExprVec axs)
loop
according to the fast option. In particular, sets
loop.desugared
to the desugaring.
private GuardedCmd wrapUpUnrolledIteration(java.lang.String locString, int iteration, GenericVarDeclVec tempVars)
private void addLoopDecreases(LoopCmd loop, int piece)
code
the various pieces of the translation of the
decreases pragma. The pieces are:
public GuardedCmd modifyATargets(Set aTargets, int loc)
public GuardedCmd modify(Set simpleTargets, int loc)
public void desugarLoopSafe(LoopCmd loop, ExprVec axs)
loop
according to the safe option. In particular, sets
loop.desugared
to the desugaring.
private void checkLoopInvariants(LoopCmd loop, ExprVec axs)
private GuardedCmd traceInfoLabelCmd(ASTNode ast, java.lang.String traceInfoTag)
private GuardedCmd traceInfoLabelCmd(ASTNode ast, java.lang.String traceInfoTag, int loc)
private GuardedCmd traceInfoLabelCmd(int sloc, int eloc, java.lang.String traceInfoTag, int loc)
private GuardedCmd traceInfoLabelCmd(int sloc, int eloc, java.lang.String traceInfoTag, java.lang.String sortSeq)
private GuardedCmd cloneGuardedCommand(GuardedCmd gc)
G
that is like
gc
except that where gc
contains a mutable command,
G
contains a fresh copy of that command. Thus, the resulting
command is as good as a fresh copy of gc
, since all other guarded
commands are to be read-only after construction.There is only one mutable command, namely an "assume" command of the form:
assume (lblpos id true)where "id" is a trace label. A fresh copy of this command consists of a fresh assume command with a fresh labeled expression. However, the "id" reference may be shared in the fresh command.
private void wrapUpDeclBlock()
declaredLocals
and code
and then appends
code
with a VARINCMD (if there were any new declared locals) or a
sequence of commands (otherwise). The new code becomes the body of the
VARINCMD or the sequence of commands.
private GuardedCmd popDeclBlock()
private void trStmt(Stmt stmt, TypeDecl decl)
stmt
into a sequence of guarded commands
that are appended to code
.
Temporaries generated for expressions in stmt
are added to temporaries
, loop invariant pragmas are
added to loopinvariants
, decreases pragmas are added
to loopDecreases
, loop predicates are added to
looppredicates
, and local skolemized variables are
added to
skolemConstants
.
stmt
- the statement that is to be translated.private void trIfStmt(Expr guard, Stmt thenStmt, Stmt elseStmt, TypeDecl decl)
private void trSynchronizedBody(Expr mu, Stmt stmt, int loc, TypeDecl decl)
private void trConstructorCallStmt(ConstructorInvocation ci)
private Expr protect(boolean protect, Expr e, int loc)
protect
is true, then the expression returned will depend only on
values of temporary variables (that is, the expression returned will not be
affected by changes to program variables). If protect
is
true
, then the value returned is certain to be of type
VariableAccess
.
private Expr protect(boolean protect, Expr e, int loc, java.lang.String suffix)
private Expr ptrExpr(VarInit expr)
private Expr trExpr(boolean protect, VarInit expr)
expr
into a sequence of guarded commands that are
appended to code
and return an expression denoting the value of
the expression. New temporaries may be generated; these are added to
temporaries
.
protect
- if true, then the expression return will depend only on values
of temporary variables (that is, the expression returned will not be affected
by changes in program variables).private static Expr addRelAsgCast(Expr rval, Type lType, Type rType)
private static Expr predEvathangsAnArray(VariableAccess allocOld, VariableAccess allocNew)
(FORALL o :: !isAllocated(o, allocOld) && isAllocated(o, allocNew) ==> isNewArray(o))
private static Expr predArrayOwnerNull(VariableAccess allocOld, VariableAccess allocNew, VariableAccess arr)
(FORALL o :: !isAllocated(o, allocOld) && isAllocated(o, allocNew) ==> o.owner == null)
public static boolean isFinal(Type t)
t
.final
modifier. Array types
are "final" if their element types satisfy isFinal
. Primitive
types are "final".private Expr trFieldAccess(boolean protectObject, FieldAccess fa)
VariableAccess
if fa
is a class
variable or a SELECT
application if fa
is an
instance variable access, or an ARRAYLENGTH
application if
fa
is the final array field length
. In the second
case, will emit code for computing the object designator and also a check to
ensure that object is not null.
private Expr trMethodInvocation(boolean protect, MethodInvocation mi)
private void nullCheck(VarInit E, Expr e, int loc)
loc
that guarded command expression
e
, which was translated from the Java expression E
,
is not null
. If E
denotes an expression that is
guaranteed not to be null
, no check is emitted.
private void nullCheck(VarInit E, Expr e, int loc, int errorName, int locPragma)
private VarInit trim(VarInit E)
E
and returns the result
private void arrayAccessCheck(Expr Array, Expr array, Expr Index, Expr index, int locOpenBracket)
array
is non-null and that
index
is inbounds for array
. Implements the
ArrayAccessCheck function of ESCJ16.
private void readCheck(Expr va, int locId)
This method implements ReadCheck as defined in ESCJ16. Handles reads of local, class, and instance variables (ESCJ16 splits these into two ReadCheck functions).
va
- is the variable being read; it must be either a
VariableAccess
(in the case of local variables and class fields)
or a SELECT
NaryExpr
(in the case of instance
fields).locId
- is the location of the variable or field being read. It is used
to determine the location of the "wrong" part of the check's label.private void writeCheck(Expr va, VarInit Rval, Expr rval, int locAssignOp, boolean inInitializerContext)
va
- is the variable being written; it must be either a
VariableAccess
(in the case of local variables and class fields)
or a SELECT
NaryExpr
(in the case of instance
fields).rval
- is the guarded command expression being written into
va
. The argument Rval
is either the Java expression
from which rval
was translated, or null
if
rval
was somehow synthesized.locAssignOp
- is the location of the assignment operator that prescribes
the write. It is used to determine the location of the "wrong" part of the
check's label.inInitializerContext
- indicates whether or not the expression whose
write check is to be performed is the initializing expression of a field.private java.util.Hashtable initializeRWCheckSubstMap(java.util.Hashtable prevMap, Expr actualSelf, int loc)
private void addCheck(int locUse, Condition cond)
GC.check
to create a check and appends the result to
code
.
void addCheck(int locUse, int errorName, Expr pred)
GC.check
to create a check and appends the result to
code
.
private void addCheck(ASTNode use, int errorName, Expr pred)
GC.check
to create a check and appends the result to
code
.
private void addCheck(int locUse, int errorName, Expr pred, int locPragmaDecl)
GC.check
to create a check and appends the result to
code
.
void addCheck(int locUse, int errorName, Expr pred, int locPragmaDecl, int auxLoc)
private void addCheck(int locUse, int errorName, Expr pred, int locPragmaDecl, java.lang.Object aux)
GC.check
to create a check and appends the result to
code
.
private void addCheck(int locUse, int errorName, Expr pred, ASTNode prag)
GC.check
to create a check and appends the
result to code
.
private void addAssumption(Expr pred)
private void addAssumptions(ExprVec ev)
private void addNewAssumptions()
ExprVec addNewAssumptionsNow()
private void addNewAssumptionsNow(ExprVec ev)
private void addNewAssumptionsHelper()
private static VariableAccess getInitVar(GenericVarDecl d)
VariableAccesss
associated with d
by a
call to setInitVar
. If none has been associated with
d
, returns null
.
private static void setInitVar(GenericVarDecl d, VariableAccess init)
init
with d
; will be returned by a call
to getInitVar
.
private GuardedCmd modify(VariableAccess va, int loc)
private GuardedCmd modify(Expr e, java.util.Hashtable pt, int loc)
private Call call(RoutineDecl rd, ExprVec argsRaw, ExprVec args, FindContributors scope, int scall, int ecall, int locOpenParen, boolean superOrSiblingConstructorCall, InlineSettings inline, Expr eod, boolean freshResult)
private InlineSettings computeInlineSettings(RoutineDecl rd, ExprVec argsRaw, InlineSettings inline, int scall)
null
means "don't inline".
public static void globallyTurnOffChecks(boolean flag)
private static GuardedCmd substituteGC(java.util.Hashtable pt, GuardedCmd gc)
public static void addTraceLabelSequenceNumbers(GuardedCmd gc)
gc
to insert sequence
numbers that are used by the ErrorMsg class in printing trace labels in the
correct execution order. This method requires that trace labels do not yet
contain sequence numbers.
private static int orderTraceLabels(GuardedCmd gc, int count)
private static int orderTraceLabel(LabelExpr le, int count)
count
number to the
given label expression's label name, so that trace labels will sort correctly.
private VariableAccess fresh(VarInit e, int loc)
This partially implements ESCJ 23b, case 6.
private VariableAccess fresh(VarInit e, int loc, java.lang.String suffix)
private VariableAccess temporary(java.lang.String s, int locAccess)
s
and associated
expression location information locAccess
.
private VariableAccess temporary(java.lang.String s, int locAccess, int locIdDecl)
public static Expr mapLocation(Expr e, int loc)
public void addMoreLocations(java.util.Set s)
static void setop(ASTNode e)
public Expr addNewString(VarInit x, Expr left, Expr right)
public VariableAccess cacheValue(Expr e)
|
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 |