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

Uses of Class
javafe.ast.Expr

Packages that use Expr
escjava   
escjava.ast   
escjava.backpred   
escjava.pa   
escjava.parser   
escjava.sp   
escjava.tc   
escjava.translate   
javafe.ast   
javafe.parser   
javafe.tc   
 

Uses of Expr in escjava
 

Subclasses of Expr in escjava
static class AnnotationHandler.NonNullExpr
           
 

Fields in escjava declared as Expr
 Expr AnnotationHandler.Context.expr
           
 

Methods in escjava that return Expr
 Expr AnnotationHandler.forallWrap(GenericVarDeclVec foralls, Expr e)
           
static Expr AnnotationHandler.and(Expr e1, Expr e2)
          Produces an expression which is the conjunction of the two expressions.
static Expr AnnotationHandler.implies(Expr e1, Expr e2)
          Produces an expression which is the implication of the two expressions.
 

Methods in escjava with parameters of type Expr
static void ProverManager.push(Expr vc)
           
static java.util.Enumeration ProverManager.prove(Expr vc, FindContributors scope)
           
 int Main.doProving(Expr vc, RoutineDecl r, Set directTargets, FindContributors scope)
           
private  void AnnotationHandler.checkMaybeAdd(Expr e, TypeNameVec tv, int locThrows)
           
private  boolean AnnotationHandler.isInSignalsOnlyExpr(Type t, Expr e, boolean allowSuperTypes)
           
static VarExprModifierPragma AnnotationHandler.defaultSignalsOnly(RoutineDecl tde, Expr req)
           
static ModifiesGroupPragma AnnotationHandler.defaultModifies(int loc, Expr req, RoutineDecl rd)
           
 Expr AnnotationHandler.forallWrap(GenericVarDeclVec foralls, Expr e)
           
static Expr AnnotationHandler.and(Expr e1, Expr e2)
          Produces an expression which is the conjunction of the two expressions.
static Expr AnnotationHandler.implies(Expr e1, Expr e2)
          Produces an expression which is the implication of the two expressions.
(package private) static boolean AnnotationHandler.isTrue(Expr e)
          Returns true if the argument is literally true, and returns false if it is not a literal or is literally false.
(package private) static boolean AnnotationHandler.isFalse(Expr e)
          Returns true if the argument is literally false, and returns false if it is not a literal or is literally true.
private static void AnnotationHandler.print(Expr e)
           
 

Uses of Expr in escjava.ast
 

Subclasses of Expr in escjava.ast
 class ArrayRangeRefExpr
           
 class DefPredApplExpr
           
 class DefPredLetExpr
           
 class EverythingExpr
           
 class GCExpr
           
 class GeneralizedQuantifiedExpr
           
 class GuardExpr
           
 class LabelExpr
           
 class LockSetExpr
           
 class NaryExpr
           
 class NothingExpr
           
 class NotModifiedExpr
           
 class NotSpecifiedExpr
           
 class NumericalQuantifiedExpr
           
 class QuantifiedExpr
           
 class ResExpr
           
 class SetCompExpr
           
 class SubstExpr
           
 class TypeExpr
           
 class WildRefExpr
           
 

Fields in escjava.ast declared as Expr
 Expr WildRefExpr.var
           
 Expr VarExprModifierPragma.expr
           
 Expr SubSubGetsCmd.index1
           
 Expr SubSubGetsCmd.index2
           
 Expr SubstExpr.val
           
 Expr SubstExpr.target
           
 Expr SubGetsCmd.index
           
 Expr SetStmtPragma.target
           
 Expr SetStmtPragma.value
           
 Expr SetCompExpr.expr
           
 Expr ReachModifierPragma.expr
           
 Expr QuantifiedExpr.rangeExpr
           
 Expr QuantifiedExpr.expr
           
 Expr NumericalQuantifiedExpr.rangeExpr
           
 Expr NumericalQuantifiedExpr.expr
           
 Expr NotModifiedExpr.expr
           
 Expr NamedExprDeclPragma.expr
           
 Expr NamedExprDeclPragma.target
           
 Expr ModifiesGroupPragma.precondition
           
 Expr MapsExprModifierPragma.mapsexpr
           
 Expr MapsExprModifierPragma.expr
           
 Expr LabelExpr.expr
           
 Expr IdExprDeclPragma.expr
           
 Expr GuardExpr.expr
           
 Expr GeneralizedQuantifiedExpr.expr
           
 Expr GeneralizedQuantifiedExpr.rangeExpr
           
 Expr ExprStmtPragma.expr
           
 Expr ExprStmtPragma.label
           
 Expr ExprModifierPragma.expr
           
 Expr ExprDeclPragma.expr
           
 Expr ExprCmd.pred
           
 Expr DependsPragma.target
           
 Expr DefPredLetExpr.body
           
 Expr DefPred.body
           
 Expr DecreasesInfo.f
           
 Expr Condition.pred
           
 Expr CondExprModifierPragma.expr
           
 Expr CondExprModifierPragma.cond
           
 Expr AssignCmd.rhs
           
 Expr ArrayRangeRefExpr.array
           
 Expr ArrayRangeRefExpr.lowIndex
           
 Expr ArrayRangeRefExpr.highIndex
           
 

Methods in escjava.ast with parameters of type Expr
static WildRefExpr WildRefExpr.make(Expr var, ObjectDesignator od)
           
static VarExprModifierPragma VarExprModifierPragma.make(int tag, GenericVarDecl arg, Expr expr, int loc)
           
static boolean Utils.isModel(Expr e)
           
static SubSubGetsCmd SubSubGetsCmd.make(VariableAccess v, Expr rhs, Expr index1, Expr index2)
           
static SubstExpr SubstExpr.make(int sloc, int eloc, GenericVarDecl var, Expr val, Expr target)
           
static SubGetsCmd SubGetsCmd.make(VariableAccess v, Expr rhs, Expr index)
           
static SetStmtPragma SetStmtPragma.make(Expr target, int locOp, Expr value, int loc)
           
static SetCompExpr SetCompExpr.make(Type type, FormalParaDecl fp, Expr expr)
           
static RestoreFromCmd RestoreFromCmd.make(VariableAccess v, Expr rhs)
           
static ReachModifierPragma ReachModifierPragma.make(Expr expr, Identifier id, IdentifierVec storerefs, int loc)
           
static QuantifiedExpr QuantifiedExpr.make(int sloc, int eloc, int quantifier, GenericVarDeclVec vars, Expr rangeExpr, Expr expr, ExprVec nopats, ExprVec pats)
           
static NumericalQuantifiedExpr NumericalQuantifiedExpr.make(int sloc, int eloc, int quantifier, GenericVarDeclVec vars, Expr rangeExpr, Expr expr, ExprVec nopats)
           
static NotModifiedExpr NotModifiedExpr.make(int loc, Expr expr)
           
static NamedExprDeclPragma NamedExprDeclPragma.make(int tag, Expr expr, Expr target, int modifiers, int loc)
           
static ModifiesGroupPragma ModifiesGroupPragma.make(int tag, CondExprModifierPragmaVec items, Expr precondition, int clauseLoc)
           
static MapsExprModifierPragma MapsExprModifierPragma.make(int tag, Identifier id, Expr mapsexpr, int loc, Expr expr)
           
static LabelExpr LabelExpr.make(int sloc, int eloc, boolean positive, Identifier label, Expr expr)
           
static IdExprDeclPragma IdExprDeclPragma.make(int tag, Identifier id, Expr expr, int modifiers, int loc, int locId)
           
static GuardExpr GuardExpr.make(Expr expr, int locPragmaDecl)
           
static GetsCmd GetsCmd.make(VariableAccess v, Expr rhs)
           
static GeneralizedQuantifiedExpr GeneralizedQuantifiedExpr.make(int sloc, int eloc, int quantifier, GenericVarDeclVec vars, Expr expr, Expr rangeExpr, ExprVec nopats)
           
static ExprStmtPragma ExprStmtPragma.make(int tag, Expr expr, Expr label, int loc)
           
static ExprModifierPragma ExprModifierPragma.make(int tag, Expr expr, int loc)
           
static ExprDeclPragma ExprDeclPragma.make(int tag, Expr expr, int modifiers, int loc)
           
static ExprCmd ExprCmd.make(int cmd, Expr pred, int loc)
           
static DependsPragma DependsPragma.make(int tag, Expr target, ExprVec exprs, int loc)
           
static DefPredLetExpr DefPredLetExpr.make(DefPredVec preds, Expr body)
           
static DefPred DefPred.make(Identifier predId, GenericVarDeclVec args, Expr body)
           
static Condition Condition.make(int label, Expr pred, int locPragmaDecl)
           
static CondExprModifierPragma CondExprModifierPragma.make(int tag, Expr expr, int loc, Expr cond)
           
static ArrayRangeRefExpr ArrayRangeRefExpr.make(int locOpenBracket, Expr array, Expr lowIndex, Expr highIndex)
           
 

Constructors in escjava.ast with parameters of type Expr
DecreasesInfo(int loc, Expr f, VariableAccess fOld)
           
 

Uses of Expr in escjava.backpred
 

Methods in escjava.backpred that return Expr
protected static Expr BackPred.eq(Expr e1, Expr e2, Type t)
          Generate the appropriate GC equality e1 == e2 based on type t.
 

Methods in escjava.backpred with parameters of type Expr
private static void BackPred.genFinalInitInfo(VarInit initExpr, GenericVarDecl sDecl, Expr s, Expr x, Type type, int loc, java.io.PrintStream proverStream)
           
private static void BackPred.produce(GenericVarDecl sDecl, Expr s, Expr e, java.io.PrintStream proverStream)
           
protected static LiteralExpr BackPred.eval(Expr e, int loc)
          Like ConstantExpr.eval, but returns a LiteralExpr instead of an Integer/Long/etc.
protected static Expr BackPred.eq(Expr e1, Expr e2, Type t)
          Generate the appropriate GC equality e1 == e2 based on type t.
 

Uses of Expr in escjava.pa
 

Methods in escjava.pa that return Expr
(package private)  Expr GCProver.concretize(mocha.wrappers.jbdd.jbdd b)
           
 

Methods in escjava.pa with parameters of type Expr
private static boolean PredicateAbstraction.mentions(Expr e, GenericVarDecl d)
           
private  void PredicateAbstraction.guessPredicate(Expr e, Expr eOld, Type type, ExprVec predicates, int loc, Expr sca, ExprVec boundsSC)
           
 

Uses of Expr in escjava.parser
 

Methods in escjava.parser that return Expr
protected  Expr EscPragmaParser.parsePrimaryExpression(Lex l)
          Parse a "primary expression" from l.
protected  Expr EscPragmaParser.parsePrimarySuffix(Lex l, Expr primary)
          Parse the suffix of a "primary expression" from l, given the prefix primary expression primary.
 Expr EscPragmaParser.parseStoreRef(EscPragmaLex l)
          Parse a StoreRef
 Expr EscPragmaParser.parseStoreRefExpr(EscPragmaLex l)
          Parse a StoreRefExpr
 Expr EscPragmaParser.parseMapsMemberFieldRef(Lex scanner)
           
 

Methods in escjava.parser with parameters of type Expr
protected  Expr EscPragmaParser.parsePrimarySuffix(Lex l, Expr primary)
          Parse the suffix of a "primary expression" from l, given the prefix primary expression primary.
 

Uses of Expr in escjava.sp
 

Fields in escjava.sp declared as Expr
 Expr NXW.n
           
 Expr NXW.x
           
 Expr NXW.w
           
 

Methods in escjava.sp that return Expr
 Expr VarMap.get(GenericVarDecl v)
           
 Expr VarMap.apply(Expr e)
          Returns the result of applying "this", viewed as a substituiton, to "e".
static Expr SPVC.compute(GuardedCmd g)
           
private  Expr SPVC.name(Expr e)
           
private  Expr SPVC.computeNotWrong(GuardedCmd root)
           
static Expr SPVC.computeN(GuardedCmd g)
           
 

Methods in escjava.sp with parameters of type Expr
 VarMap VarMap.extend(GenericVarDecl v, Expr e)
          Returns a VarMap identical to "this", except mapping "v" to "e".
 Expr VarMap.apply(Expr e)
          Returns the result of applying "this", viewed as a substituiton, to "e".
private  Expr SPVC.name(Expr e)
           
static boolean SPVC.isSimpleConjunction(Expr e)
           
private static boolean SPVC.isSimpleExpr(Expr e)
           
 

Uses of Expr in escjava.tc
 

Methods in escjava.tc that return Expr
protected  Expr FlowInsensitiveChecks.checkPredicate(Env env, Expr e)
           
protected  Expr FlowInsensitiveChecks.checkExpr(Env env, Expr e)
           
 

Methods in escjava.tc with parameters of type Expr
protected  Expr FlowInsensitiveChecks.checkPredicate(Env env, Expr e)
           
protected  Expr FlowInsensitiveChecks.checkExpr(Env env, Expr e)
           
 int FlowInsensitiveChecks.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.
protected  boolean FlowInsensitiveChecks.assignmentConvertable(Expr e, Type t)
           
static void Datagroups.add(TypeDecl td, FieldDecl fd, Expr fa)
          Add Expr fa to the datagroup for declaration fd in the context of type td; the declaration fd may be in a superclass.
 

Uses of Expr in escjava.translate
 

Fields in escjava.translate declared as Expr
(package private)  Expr InvariantInfo.J
           
protected static Expr TrAnExpr.specialResultExpr
          This is the full form of function TrSpecExpr described in ESCJ 16.
protected static Expr TrAnExpr.specialThisExpr
           
static Expr Substitute.resexpr
           
static Expr Substitute.thisexpr
           
private  Expr InitialState.is
           
static Expr GC.nulllit
           
static Expr GC.zerolit
           
static Expr GC.onelit
           
static Expr GC.truelit
           
static Expr GC.falselit
           
static Expr GC.dzerolit
           
static Expr GC.ec_throw
           
static Expr GC.ec_return
           
 Expr[] ATarget.indices
           
private static Expr ATarget.nonConst
           
 

Methods in escjava.translate that return Expr
private  Expr Translate.breakLabel(Stmt s)
           
private  Expr Translate.continueLabel(Stmt s)
           
private  Expr Translate.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 Translate.protect(boolean protect, Expr e, int loc, java.lang.String suffix)
           
private  Expr Translate.ptrExpr(VarInit expr)
          Purify and translate expr without protection
private  Expr Translate.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 static Expr Translate.addRelAsgCast(Expr rval, Type lType, Type rType)
           
private static Expr Translate.predEvathangsAnArray(VariableAccess allocOld, VariableAccess allocNew)
          Returns the guarded-command expression: (FORALL o :: !
private static Expr Translate.predArrayOwnerNull(VariableAccess allocOld, VariableAccess allocNew, VariableAccess arr)
          Returns the guarded-command expression: (FORALL o :: !
private  Expr Translate.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  Expr Translate.trMethodInvocation(boolean protect, MethodInvocation mi)
          This translation of method invocation follows section 4.1 of ESCJ 16.
static Expr Translate.mapLocation(Expr e, int loc)
           
 Expr Translate.addNewString(VarInit x, Expr left, Expr right)
           
static Expr TrAnExpr.trSpecExpr(Expr e)
          This is the abbreviated form of function TrSpecExpr described in ESCJ 16.
static Expr TrAnExpr.trSpecExpr(Expr e, Expr thisExpr)
           
static Expr TrAnExpr.trSpecExpr(Expr e, java.util.Hashtable sp, java.util.Hashtable st, Expr thisExpr)
           
static Expr TrAnExpr.trSpecExpr(Expr e, java.util.Hashtable sp, java.util.Hashtable st)
           
 Expr TrAnExpr.trSpecExprI(Expr e, java.util.Hashtable sp, java.util.Hashtable st)
           
static Expr TrAnExpr.targetTypeCorrect(GenericVarDecl vd, java.util.Hashtable wt)
          This method implements the ESCJ 16 function TargetTypeCorrect, except for the init$ case!
static Expr TrAnExpr.typeCorrect(GenericVarDecl vd)
          This method implements the ESCJ 16 function TypeCorrect.
static Expr TrAnExpr.typeCorrect(GenericVarDecl vd, java.util.Hashtable sp)
           
static Expr TrAnExpr.quantTypeCorrect(GenericVarDecl vd, java.util.Hashtable sp)
           
static Expr TrAnExpr.resultEqualsCall(GenericVarDecl vd, RoutineDecl rd, java.util.Hashtable sp)
           
static Expr TrAnExpr.typeCorrectAs(GenericVarDecl vd, Type type)
           
static Expr TrAnExpr.typeAndNonNullCorrectAs(GenericVarDecl vd, Type type, SimpleModifierPragma nonNullPragma, boolean forceNonNull, java.util.Hashtable sp)
           
static Expr TrAnExpr.fieldTypeCorrect(FieldDecl fdecl)
           
static Expr TrAnExpr.elemsTypeCorrect(GenericVarDecl edecl)
           
static Expr TrAnExpr.getEquivalentAxioms(RepHelper o, java.util.Hashtable sp)
           
private static Expr TrAnExpr.createFunctionCall(RoutineDecl rd, java.util.ArrayList bounds, java.util.Hashtable sp)
           
private static Expr TrAnExpr.createForall(Expr expr, Expr fcall, java.util.ArrayList bounds)
           
static Expr TrAnExpr.getRepresentsAxiom(NamedExprDeclPragma p, java.util.Hashtable sp)
          Translates an individual represents clause into a class-level axiom.
static Expr Substitute.doSubst(java.util.Hashtable subst, Expr e)
          Does substitution on GCExprs union (resolved) SpecExprs.
static Expr Substitute.doSimpleSubst(java.util.Hashtable subst, Expr e)
           
private static Expr Substitute.doSubst(java.util.Hashtable subst, Expr e, Substitute.SetRef rhsVars)
          Does substitution on GCExprs union (resolved) SpecExprs.
(package private) static Expr Inner.unfoldThis(ThisExpr t)
          * Converts a 1.1 ThisExpr of the form .this into an Java * 1.0 expression of the form this.this$0.this$0.this$0...
 Expr InitialState.getInitialState()
           
static Expr GC.subst(int sloc, int eloc, java.util.Hashtable subst, Expr target)
           
static Expr GC.subst(int sloc, int eloc, GenericVarDecl var, Expr val, Expr target)
           
static Expr GC.subst(GenericVarDecl var, Expr val, Expr target)
           
static Expr GC.symlit(java.lang.String s)
           
static Expr GC.symlit(Stmt s, java.lang.String prefix)
           
static Expr GC.zeroequiv(Type t)
           
static Expr GC.typeExpr(Type t)
           
static Expr GC.cast(Expr e, Type t)
           
static Expr GC.nary(int tag, Expr e)
           
static Expr GC.nary(int sloc, int eloc, int tag, Expr e)
           
static Expr GC.nary(int tag, Expr e1, Expr e2)
           
static Expr GC.nary(int sloc, int eloc, int tag, Expr e1, Expr e2)
           
static Expr GC.nary(int tag, Expr e1, Expr e2, Expr e3)
           
static Expr GC.nary(int sloc, int eloc, int tag, Expr e1, Expr e2, Expr e3)
           
static Expr GC.nary(int tag, ExprVec ev)
           
static Expr GC.nary(Identifier id, ExprVec ev)
           
static Expr GC.nary(Identifier id, Expr e)
           
static Expr GC.nary(Identifier id, Expr e1, Expr e2)
           
static Expr GC.nary(int sloc, int eloc, Identifier id, ExprVec ev)
           
static Expr GC.nary(int sloc, int eloc, int tag, ExprVec ev)
           
static Expr GC.select(Expr c0, Expr c1)
           
static Expr GC.not(Expr c)
           
static Expr GC.not(int sloc, int eloc, Expr c)
           
static Expr GC.and(Expr c1, Expr c2)
           
static Expr GC.andx(Expr c1, Expr c2)
           
static Expr GC.and(int sloc, int eloc, Expr c1, Expr c2)
           
static Expr GC.and(ExprVec v)
           
static Expr GC.and(int sloc, int eloc, ExprVec v)
           
static Expr GC.or(Expr c1, Expr c2)
           
static Expr GC.or(int sloc, int eloc, Expr c1, Expr c2)
           
static Expr GC.or(ExprVec v)
           
static Expr GC.or(int sloc, int eloc, ExprVec v)
           
static Expr GC.implies(Expr c0, Expr c1)
           
static Expr GC.implies(int sloc, int eloc, Expr c0, Expr c1)
           
static Expr GC.forall(GenericVarDecl v, Expr e)
           
static Expr GC.forall(GenericVarDecl v, Expr range, Expr e)
           
static Expr GC.forall(GenericVarDeclVec v, Expr range, Expr e)
           
static Expr GC.forall(GenericVarDecl v, Expr e, ExprVec nopats)
           
static Expr GC.forallwithpats(GenericVarDecl v, Expr e, ExprVec pats)
           
static Expr GC.forall(int sloc, int eloc, GenericVarDecl v, Expr range, Expr e)
           
static Expr GC.forall(int sloc, int eloc, GenericVarDecl v, Expr range, Expr e, ExprVec nopats)
           
static Expr GC.quantifiedExpr(int sloc, int eloc, int tag, GenericVarDecl v, Expr range, Expr e, ExprVec nopats, ExprVec pats)
           
static Expr GC.quantifiedExpr(int sloc, int eloc, int tag, GenericVarDeclVec vs, Expr range, Expr e, ExprVec nopats, ExprVec pats)
           
private  Expr Frame.modifiesCheckFieldHelper(Expr eod, int callLoc, FieldDecl fd, int calleeLoc, Expr callee_tprecondition, boolean genExpr, ModifiesGroupPragmaVec mg, Expr thisexpr, java.util.Hashtable args)
          This is a helper method to generate checks that a particular field assignment is allowed by the frame conditions.
private  Expr Frame.modifiesCheckMethod(Expr eod, int loccall, java.util.Hashtable args, boolean freshResult, java.lang.Object calleeStoreRef, Expr callee_tprecondition, boolean genExpr, ModifiesGroupPragmaVec mg)
          Helper method that checks that a particular store-ref in the frame conditions of a called method against the frame conditions of the caller.
private  Expr Frame.modifiesCheckArray(Expr array, Expr arrayIndex, int callLoc, int calleeLoc, Expr callee_tprecondition, boolean genExpr, ModifiesGroupPragmaVec mg, Expr thisexpr, java.util.Hashtable args)
          This adds checks for whether the given array with the given index may be assigned to.
private  Expr Frame.modChecksComplete(Expr precondition, Expr tprecond2, ExprVec ev, int callLoc, int aloc, int aloc2, boolean genExpr)
          Generates the actual check with the condition 'if (precondition && tprecond2) then (disjunction of ev)'
private  Expr Frame.modTranslate(Expr e, boolean old, Expr thisexpr, java.util.Hashtable args)
          Translates the Expr e into guarded commands:
if old is true, uses the premap to map variables if old is false, uses args as the variable mapping
static Expr Ejp.compute(GuardedCmd g, Expr normal, Expr exceptional)
           
private static Expr Ejp.compute(GuardedCmd g, Expr normal, Expr exceptional, java.lang.String dynInstPrefix, VarMap dynInstMap)
           
private static Expr ATarget.applyEnv(java.util.Hashtable env, Expr expr)
          Returns null if expr not loop constant
 

Methods in escjava.translate with parameters of type Expr
static void VcToStringPvs.computeTypeSpecific(Expr e, java.io.PrintStream to)
          Prints e as a simple-expression string to to.
static void VcToStringPvs.compute(Expr e, java.io.PrintStream to)
          Prints e as a verification-condition string to to.
static void VcToStringPvs.computePC(Expr e, java.io.PrintStream to)
           
protected  java.lang.String VcToStringPvs.vc2Term(Expr e, java.util.Hashtable subst)
           
protected  DefPredVec VcToStringPvs.getDefpreds(Expr e)
           
protected  void VcToStringPvs.getDefpredsHelper(Expr e)
           
protected  void VcToStringPvs.printFormula(java.io.PrintStream out, Expr e)
           
protected  void VcToStringPvs.printFormula(java.io.PrintStream out, java.util.Hashtable subst, Expr e)
           
protected  void VcToStringPvs.reallyPrintFormula(java.io.PrintStream out, java.util.Hashtable subst, Expr e)
           
protected  void VcToStringPvs.printTerm(java.io.PrintStream out, java.util.Hashtable subst, Expr e)
           
static void VcToString.computeTypeSpecific(Expr e, java.io.PrintStream to)
          Prints e as a simple-expression string to to.
static void VcToString.compute(Expr e, java.io.PrintStream to)
          Prints e as a verification-condition string to to.
static void VcToString.computePC(Expr e, java.io.PrintStream to)
           
protected  java.lang.String VcToString.vc2Term(Expr e, java.util.Hashtable subst)
           
protected  DefPredVec VcToString.getDefpreds(Expr e)
           
protected  void VcToString.getDefpredsHelper(Expr e)
           
protected  void VcToString.printFormula(java.io.PrintStream out, Expr e)
           
protected  void VcToString.printFormula(java.io.PrintStream out, java.util.Hashtable subst, Expr e)
           
protected  void VcToString.reallyPrintFormula(java.io.PrintStream out, java.util.Hashtable subst, Expr e)
           
protected  void VcToString.printTerm(java.io.PrintStream out, java.util.Hashtable subst, Expr e)
           
private  GuardedCmd Translate.opBlockCmd(Expr label)
          Reduces number of stack marks by 1.
private  void Translate.raise(Expr label)
          Emits the commands EC= label; raise to code.
private  void Translate.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  void Translate.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.
private  void Translate.trIfStmt(Expr guard, Stmt thenStmt, Stmt elseStmt, TypeDecl decl)
          Translate an "if" statement.
private  void Translate.trSynchronizedBody(Expr mu, Stmt stmt, int loc, TypeDecl decl)
           
private  Expr Translate.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 Translate.protect(boolean protect, Expr e, int loc, java.lang.String suffix)
           
private static Expr Translate.addRelAsgCast(Expr rval, Type lType, Type rType)
           
private  void Translate.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 Translate.nullCheck(VarInit E, Expr e, int loc, int errorName, int locPragma)
           
private  void Translate.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  void Translate.readCheck(Expr va, int locId)
          Insert checks done before reading variables.
private  void Translate.writeCheck(Expr va, VarInit Rval, Expr rval, int locAssignOp, boolean inInitializerContext)
          Insert checks done before writing variables, as prescribed by WriteCheck in ESCJ 16.
private  java.util.Hashtable Translate.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).
(package private)  void Translate.addCheck(int locUse, int errorName, Expr pred)
          Calls GC.check to create a check and appends the result to code.
private  void Translate.addCheck(ASTNode use, int errorName, Expr pred)
          Calls GC.check to create a check and appends the result to code.
private  void Translate.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 Translate.addCheck(int locUse, int errorName, Expr pred, int locPragmaDecl, int auxLoc)
           
private  void Translate.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 Translate.addCheck(int locUse, int errorName, Expr pred, ASTNode prag)
          Calls GC.check to create a check and appends the result to code.
private  void Translate.addAssumption(Expr pred)
           
private  GuardedCmd Translate.modify(Expr e, java.util.Hashtable pt, int loc)
           
private  Call Translate.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.
static Expr Translate.mapLocation(Expr e, int loc)
           
 Expr Translate.addNewString(VarInit x, Expr left, Expr right)
           
 VariableAccess Translate.cacheValue(Expr e)
           
 void Translate.EverythingLoc.add(Expr e)
           
static Expr TrAnExpr.trSpecExpr(Expr e)
          This is the abbreviated form of function TrSpecExpr described in ESCJ 16.
static Expr TrAnExpr.trSpecExpr(Expr e, Expr thisExpr)
           
static Expr TrAnExpr.trSpecExpr(Expr e, java.util.Hashtable sp, java.util.Hashtable st, Expr thisExpr)
           
static Expr TrAnExpr.trSpecExpr(Expr e, java.util.Hashtable sp, java.util.Hashtable st)
           
 Expr TrAnExpr.trSpecExprI(Expr e, java.util.Hashtable sp, java.util.Hashtable st)
           
static void TrAnExpr.getCalledSpecs(RoutineDecl decl, ObjectDesignator od, ExprVec ev, Expr resultVar, java.util.Hashtable sp, java.util.Hashtable st)
           
private static Expr TrAnExpr.createForall(Expr expr, Expr fcall, java.util.ArrayList bounds)
           
private static java.lang.String Suggestion.gInvariant(Expr E, RoutineDecl rd, SList cc, int locDecl)
           
private static Set Suggestion.possiblyInjectiveFields(Expr e)
           
static Expr Substitute.doSubst(java.util.Hashtable subst, Expr e)
          Does substitution on GCExprs union (resolved) SpecExprs.
static Expr Substitute.doSimpleSubst(java.util.Hashtable subst, Expr e)
           
private static Expr Substitute.doSubst(java.util.Hashtable subst, Expr e, Substitute.SetRef rhsVars)
          Does substitution on GCExprs union (resolved) SpecExprs.
static boolean Substitute.mentionsFresh(Expr e)
           
private static VariableAccess GetSpec.shave(Expr e)
          Shaves a GC designator.
private static boolean GetSpec.exprIsVisible(TypeSig originType, Expr e)
           
static void GetSpec.collectFields(Expr e, java.util.Set s)
           
private static void GCSanity.checkUses(Expr e, Set cdni, Set euei, Set uuei)
           
static GuardedCmd GC.gets(VariableAccess lhs, Expr rhs)
           
static GuardedCmd GC.subgets(VariableAccess lhs, Expr index, Expr rhs)
           
static GuardedCmd GC.subsubgets(VariableAccess lhs, Expr array, Expr index, Expr rhs)
           
static GuardedCmd GC.restoreFrom(VariableAccess lhs, Expr rhs)
           
static GuardedCmd GC.ifcmd(Expr t, GuardedCmd c, GuardedCmd a)
           
static boolean GC.isBooleanLiteral(Expr e, boolean b)
          Returns true when e is a boolean literal expression whose value is b.
static boolean GC.isFalse(Expr e)
          Returns true only if e represents an expression equivalent to false.
static GuardedCmd GC.check(int locUse, int errorName, Expr pred, int locPragmaDecl)
          Creates an assert, assume, or skip command, depending on the kind of given error name and locations, and depending on what checks are enabled where.
static GuardedCmd GC.check(int locUse, int errorName, Expr pred, int locPragmaDecl, java.lang.Object aux)
           
static GuardedCmd GC.check(int locUse, int errorName, Expr pred, int locPragmaDecl, int auxLoc, java.lang.Object aux)
           
static Condition GC.condition(int label, Expr pred, int locPragmaDecl)
           
static Condition GC.freeCondition(Expr pred, int locPragmaDecl)
           
static Condition GC.assumeCondition(Expr pred, int locPragmaDecl)
           
static GuardedCmd GC.assumeAnnotation(int locPragmaDecl, Expr p)
           
static GuardedCmd GC.assume(Expr p)
           
static GuardedCmd GC.assumeNegation(Expr p)
           
private static GuardedCmd GC.assertPredicate(int locUse, int errorName, Expr pred, int locPragmaDecl, int auxLoc, java.lang.Object aux)
           
static Expr GC.subst(int sloc, int eloc, java.util.Hashtable subst, Expr target)
           
static Expr GC.subst(int sloc, int eloc, GenericVarDecl var, Expr val, Expr target)
           
static Expr GC.subst(GenericVarDecl var, Expr val, Expr target)
           
static Expr GC.cast(Expr e, Type t)
           
static Expr GC.nary(int tag, Expr e)
           
static Expr GC.nary(int sloc, int eloc, int tag, Expr e)
           
static Expr GC.nary(int tag, Expr e1, Expr e2)
           
static Expr GC.nary(int sloc, int eloc, int tag, Expr e1, Expr e2)
           
static Expr GC.nary(int tag, Expr e1, Expr e2, Expr e3)
           
static Expr GC.nary(int sloc, int eloc, int tag, Expr e1, Expr e2, Expr e3)
           
static Expr GC.nary(Identifier id, Expr e)
           
static Expr GC.nary(Identifier id, Expr e1, Expr e2)
           
static Expr GC.select(Expr c0, Expr c1)
           
static Expr GC.not(Expr c)
           
static Expr GC.not(int sloc, int eloc, Expr c)
           
static Expr GC.and(Expr c1, Expr c2)
           
static Expr GC.andx(Expr c1, Expr c2)
           
static Expr GC.and(int sloc, int eloc, Expr c1, Expr c2)
           
static Expr GC.or(Expr c1, Expr c2)
           
static Expr GC.or(int sloc, int eloc, Expr c1, Expr c2)
           
static Expr GC.implies(Expr c0, Expr c1)
           
static Expr GC.implies(int sloc, int eloc, Expr c0, Expr c1)
           
static Expr GC.forall(GenericVarDecl v, Expr e)
           
static Expr GC.forall(GenericVarDecl v, Expr range, Expr e)
           
static Expr GC.forall(GenericVarDeclVec v, Expr range, Expr e)
           
static Expr GC.forall(GenericVarDecl v, Expr e, ExprVec nopats)
           
static Expr GC.forallwithpats(GenericVarDecl v, Expr e, ExprVec pats)
           
static Expr GC.forall(int sloc, int eloc, GenericVarDecl v, Expr range, Expr e)
           
static Expr GC.forall(int sloc, int eloc, GenericVarDecl v, Expr range, Expr e, ExprVec nopats)
           
static Expr GC.quantifiedExpr(int sloc, int eloc, int tag, GenericVarDecl v, Expr range, Expr e, ExprVec nopats, ExprVec pats)
           
static Expr GC.quantifiedExpr(int sloc, int eloc, int tag, GenericVarDeclVec vs, Expr range, Expr e, ExprVec nopats, ExprVec pats)
           
static boolean GC.isSimple(Expr e)
           
private static boolean GC.selectiveAdd(ExprVec to, ExprVec from, Expr bot, Expr top, int naryTagMerge)
          Adds elements to to from from.
 boolean Frame.isDefinitelyNotAssignable(Expr eod, FieldDecl fd)
          This method returns whether the given field (fd) of the given object (eod) (which is null if the field is static) is definitely not allowed to be assigned according to the specs of the current RoutineDecl.
(package private)  void Frame.modifiesCheckField(Expr lhs, int callLoc, FieldDecl fd)
          This method generates checks that the field in lhs is allowed to be assigned according to the specification of the current RoutineDecl (rdCurrent).
private  Expr Frame.modifiesCheckFieldHelper(Expr eod, int callLoc, FieldDecl fd, int calleeLoc, Expr callee_tprecondition, boolean genExpr, ModifiesGroupPragmaVec mg, Expr thisexpr, java.util.Hashtable args)
          This is a helper method to generate checks that a particular field assignment is allowed by the frame conditions.
(package private)  void Frame.modifiesCheckMethodI(ModifiesGroupPragmaVec calleeFrameConditions, Expr eod, int loccall, java.util.Hashtable args, boolean freshResult, TypeDecl td_callee)
          This method generates checks that the locations possibly assigned by a called method are allowed to be assigned by the caller.
private  Expr Frame.modifiesCheckMethod(Expr eod, int loccall, java.util.Hashtable args, boolean freshResult, java.lang.Object calleeStoreRef, Expr callee_tprecondition, boolean genExpr, ModifiesGroupPragmaVec mg)
          Helper method that checks that a particular store-ref in the frame conditions of a called method against the frame conditions of the caller.
(package private)  void Frame.modifiesCheckArray(Expr array, Expr arrayIndex, int callLoc)
          This adds checks for whether the given array with the given index may be assigned to.
private  Expr Frame.modifiesCheckArray(Expr array, Expr arrayIndex, int callLoc, int calleeLoc, Expr callee_tprecondition, boolean genExpr, ModifiesGroupPragmaVec mg, Expr thisexpr, java.util.Hashtable args)
          This adds checks for whether the given array with the given index may be assigned to.
private  void Frame.addAllocExpression(ExprVec ev, Expr e)
          Adds an expression into ev stating that e is allocated now but was not allocated in the pre-state.
private  Expr Frame.modChecksComplete(Expr precondition, Expr tprecond2, ExprVec ev, int callLoc, int aloc, int aloc2, boolean genExpr)
          Generates the actual check with the condition 'if (precondition && tprecond2) then (disjunction of ev)'
private  Expr Frame.modTranslate(Expr e, boolean old, Expr thisexpr, java.util.Hashtable args)
          Translates the Expr e into guarded commands:
if old is true, uses the premap to map variables if old is false, uses args as the variable mapping
private  boolean Frame.isTrueLiteral(Expr p)
          A utility function that returns true if the argument expression is null or strictly equal to a boolean TRUE.
static Expr Ejp.compute(GuardedCmd g, Expr normal, Expr exceptional)
           
private static Expr Ejp.compute(GuardedCmd g, Expr normal, Expr exceptional, java.lang.String dynInstPrefix, VarMap dynInstMap)
           
private static void ATarget.addTarget(GenericVarDecl vd, Expr index)
           
private static void ATarget.addTarget(GenericVarDecl vd, Expr index1, Expr index2)
           
private static void ATarget.addTarget(GenericVarDecl vd, Expr[] indices)
           
static boolean ATarget.mentions(Expr expr, Set s)
           
private static void ATarget.extendEnv(java.util.Hashtable env, GenericVarDecl d, Expr e)
           
private static Expr ATarget.applyEnv(java.util.Hashtable env, Expr expr)
          Returns null if expr not loop constant
 

Constructors in escjava.translate with parameters of type Expr
ATarget(GenericVarDecl x, Expr[] indices)
           
 

Uses of Expr in javafe.ast
 

Subclasses of Expr in javafe.ast
 class AmbiguousMethodInvocation
          Represents a Name occuring before an argument list.
 class AmbiguousVariableAccess
          Represents a Name that occurs in an Expression position.
 class ArrayRefExpr
           
 class BinaryExpr
          Represents various kinds of binary expressions (eg +,-,|,%=, etc).
 class CastExpr
           
 class ClassLiteral
          Represents a class literal (Type . class)
 class CondExpr
           
 class FieldAccess
          Represents various kinds of field access expressions.
 class InstanceOfExpr
           
 class LiteralExpr
          Represents a Literal.
 class MethodInvocation
          Represents a MethodInvocation.
 class NewArrayExpr
           
 class NewInstanceExpr
           
 class ParenExpr
           
 class ThisExpr
          We represent [C.]this.
 class UnaryExpr
          Represents various kinds of unary expressions.
 class VariableAccess
          Represents a simple name that is bound to a local variable declaration.
 

Fields in javafe.ast declared as Expr
 Expr WhileStmt.expr
           
 Expr UnaryExpr.expr
           
 Expr ThrowStmt.expr
           
 Expr SynchronizeStmt.expr
           
 Expr SwitchStmt.expr
           
 Expr SwitchLabel.expr
           
 Expr ReturnStmt.expr
           
 Expr ParenExpr.expr
           
 Expr NewInstanceExpr.enclosingInstance
          The enclosing instance is the object expression before a new call ( .new T(...) ).
 Expr InstanceOfExpr.expr
           
 Expr IfStmt.expr
           
 Expr ForStmt.test
           
private  Expr[] ExprVec.elements
          * Instance fields: * *
 Expr ExprObjectDesignator.expr
           
 Expr EvalStmt.expr
           
 Expr DoStmt.expr
           
 Expr ConstructorInvocation.enclosingInstance
          The enclosing instance is the object expression before a super call ( .super(...) ).
 Expr CondExpr.test
           
 Expr CondExpr.thn
           
 Expr CondExpr.els
           
 Expr CastExpr.expr
           
 Expr BinaryExpr.left
           
 Expr BinaryExpr.right
           
 Expr AssertStmt.pred
           
 Expr AssertStmt.label
           
 Expr ArrayRefExpr.array
           
 Expr ArrayRefExpr.index
           
 

Methods in javafe.ast that return Expr
 Expr ExprVec.elementAt(int index)
          * Other methods: * *
 Expr[] ExprVec.toArray()
           
 Expr ExprVec.pop()
           
 

Methods in javafe.ast with parameters of type Expr
static WhileStmt WhileStmt.make(Expr expr, Stmt stmt, int loc, int locGuardOpenParen)
           
 java.lang.Object VisitorArgResult.visitExpr(Expr x, java.lang.Object o)
           
 void Visitor.visitExpr(Expr x)
           
static UnaryExpr UnaryExpr.make(int op, Expr expr, int locOp)
           
static ThrowStmt ThrowStmt.make(Expr expr, int loc)
           
static SynchronizeStmt SynchronizeStmt.make(Expr expr, BlockStmt stmt, int loc, int locOpenParen)
           
static SwitchStmt SwitchStmt.make(StmtVec stmts, int locOpenBrace, int locCloseBrace, Expr expr, int loc)
           
static SwitchLabel SwitchLabel.make(Expr expr, int loc)
           
static ReturnStmt ReturnStmt.make(Expr expr, int loc)
           
 void PrettyPrint.println(java.io.PrintStream out, Expr e)
          Writes an Expr (a type of ASTNode) to the given PrintStream, followed by an end-of-line.
static ParenExpr ParenExpr.make(Expr expr, int locOpenParen, int locCloseParen)
           
static NewInstanceExpr NewInstanceExpr.make(Expr enclosingInstance, int locDot, TypeName type, ExprVec args, ClassDecl anonDecl, int loc, int locOpenParen)
           
static InstanceOfExpr InstanceOfExpr.make(Expr expr, Type type, int loc)
           
static IfStmt IfStmt.make(Expr expr, Stmt thn, Stmt els, int loc)
           
static ForStmt ForStmt.make(StmtVec forInit, Expr test, ExprVec forUpdate, Stmt body, int loc, int locFirstSemi)
           
static ExprVec ExprVec.make(Expr[] els)
           
 void ExprVec.setElementAt(Expr x, int index)
           
 boolean ExprVec.contains(Expr x)
           
 void ExprVec.addElement(Expr x)
           
 boolean ExprVec.removeElement(Expr x)
           
 void ExprVec.insertElementAt(Expr obj, int index)
           
static ExprObjectDesignator ExprObjectDesignator.make(int locDot, Expr expr)
           
static EvalStmt EvalStmt.make(Expr expr)
           
static DoStmt DoStmt.make(Expr expr, Stmt stmt, int loc)
           
 void DefaultVisitor.visitExpr(Expr x)
           
static ConstructorInvocation ConstructorInvocation.make(boolean superCall, Expr enclosingInstance, int locDot, int locKeyword, int locOpenParen, ExprVec args)
           
static CondExpr CondExpr.make(Expr test, Expr thn, Expr els, int locQuestion, int locColon)
           
static CastExpr CastExpr.make(Expr expr, Type type, int locOpenParen, int locCloseParen)
           
static BinaryExpr BinaryExpr.make(int op, Expr left, Expr right, int locOp)
           
static AssertStmt AssertStmt.make(Expr pred, Expr label, int loc)
           
static ArrayRefExpr ArrayRefExpr.make(Expr array, Expr index, int locOpenBracket, int locCloseBracket)
           
 

Constructors in javafe.ast with parameters of type Expr
ExprVec(Expr[] els)
          * Private constructors: * *
 

Uses of Expr in javafe.parser
 

Fields in javafe.parser declared as Expr
private  Expr[] ParseExpr.exprStack
           
 

Methods in javafe.parser that return Expr
 Expr ParseExpr.parseExpression(Lex l)
          Parse an Expression.
 Expr ParseExpr.parseUnaryExpression(Lex l)
          Parse a UnaryExpression.
 Expr ParseExpr.parseCastExpression(Lex l)
          Parse a CastExpression.
protected  Expr ParseExpr.parsePrimaryExpression(Lex l)
          Parse a PrimaryExpression.
protected  Expr ParseExpr.parseClassLiteralSuffix(Lex l, Type t)
          parses '. class', then produces a class literal expression using Type t.
protected  Expr ParseExpr.parsePrimarySuffix(Lex l, Expr primary)
           
 Expr ParseExpr.parseNewExpression(Lex l)
          Parse a NewExpression.
 Expr ParseExpr.parseNewExpressionTail(Lex l, Type type, int locNew)
           
 

Methods in javafe.parser with parameters of type Expr
static boolean ParseStmt.isStatementExpression(Expr e)
           
protected  Expr ParseExpr.parsePrimarySuffix(Lex l, Expr primary)
           
 

Uses of Expr in javafe.tc
 

Methods in javafe.tc that return Expr
protected  Expr FlowInsensitiveChecks.checkDesignator(Env env, Expr e)
           
protected  Expr FlowInsensitiveChecks.checkExpr(Env env, Expr expr, Type t)
           
protected  Expr FlowInsensitiveChecks.checkExpr(Env env, Expr x)
          This method should call setType on x before its done.
 Expr Env.disambiguateExprName(Name n)
          Attempt to disambiguate an Expr Name.
 Expr Env.lookupEnclosingInstance(TypeSig T, int loc)
          Attempt to locate a current or enclosing instance that has type T.
 

Methods in javafe.tc with parameters of type Expr
protected  Expr FlowInsensitiveChecks.checkDesignator(Env env, Expr e)
           
protected  Expr FlowInsensitiveChecks.checkExpr(Env env, Expr expr, Type t)
           
protected  Expr FlowInsensitiveChecks.checkExpr(Env env, Expr x)
          This method should call setType on x before its done.
private  Type FlowInsensitiveChecks.tryCondExprMatch(Expr leftExpr, Expr rightExpr)
          Return the type of a E1 : L ?
protected  Type FlowInsensitiveChecks.checkBinaryExpr(int op, Expr left, Expr right, int loc)
           
(package private) static boolean FlowInsensitiveChecks.checkIntegralType(Expr e)
           
(package private) static boolean FlowInsensitiveChecks.checkNumericType(Expr e)
           
(package private) static boolean FlowInsensitiveChecks.isVariable(Expr e)
           
(package private) static void FlowInsensitiveChecks.checkType(Expr expr, Type t)
           
protected  boolean FlowInsensitiveChecks.assignmentConvertable(Expr e, Type t)
          Checks if Exp e can be assigned to Type t.
static java.lang.Object ConstantExpr.eval(Expr e)
          Evaluates a compile-time constant expression.
 


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

The ESC/Java2 Project Homepage