|
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.Substitute
Responsible for performing substitutions in expressions.
Nested Class Summary | |
private static class |
Substitute.SetRef
|
Field Summary | |
static Expr |
resexpr
|
static Expr |
thisexpr
|
Constructor Summary | |
Substitute()
|
Method Summary | |
static Expr |
doSimpleSubst(java.util.Hashtable subst,
Expr e)
|
static Expr |
doSubst(java.util.Hashtable subst,
Expr e)
Does substitution on GCExprs union (resolved) SpecExprs. |
private static Expr |
doSubst(java.util.Hashtable subst,
Expr e,
Substitute.SetRef rhsVars)
Does substitution on GCExprs union (resolved) SpecExprs. |
static Set |
freeVars(ASTNode e)
Calculate the free variables of an expression or a GuardedCmd. |
static boolean |
mentionsFresh(Expr e)
|
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
public static final Expr resexpr
public static final Expr thisexpr
Constructor Detail |
public Substitute()
Method Detail |
public static Expr doSubst(java.util.Hashtable subst, Expr e)
No SubstExpr's may be contained in e.
public static Expr doSimpleSubst(java.util.Hashtable subst, Expr e)
private static Expr doSubst(java.util.Hashtable subst, Expr e, Substitute.SetRef rhsVars)
No SubstExpr's may be contained in e.
rhsVars
refers to a pointer to a Set. This pointer
is either null or the set of variables (GenericVarDecl's) occurring
in right-hand sides of subst
.
public static Set freeVars(ASTNode e)
Precondition; e must be resolved, e may not contain FieldAccess as a subnode.
[mdl: I have checked that this code works with invariants translated to Exprs. I am unsure if it works correctly on anything else.] Note: length is not a free variable of translated code. (It turns into applications of the built-in function arrayLength.)
public static boolean mentionsFresh(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 |