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 NEXT | FRAMES NO FRAMES

## Uses of Class
javafe.ast.ExprVec

Packages that use ExprVec
escjava.ast |
escjava.pa |
escjava.translate |
javafe.ast |
javafe.parser |
javafe.tc |

Uses of ExprVec in escjava.ast

Fields in escjava.ast declared as ExprVec
`ExprVec` | `Spec.targets`
`ExprVec` | `Spec.specialTargets`
`ExprVec` | `Spec.preAssumptions`
`ExprVec` | `Spec.postAssumptions`
`ExprVec` | `QuantifiedExpr.nopats`
`ExprVec` | `QuantifiedExpr.pats`
`ExprVec` | `NumericalQuantifiedExpr.nopats`
`ExprVec` | `NaryExpr.exprs`
`ExprVec` | `LoopCmd.predicates`
`ExprVec` | `GeneralizedQuantifiedExpr.nopats`
`ExprVec` | `DependsPragma.exprs`
`ExprVec` | `DefPredApplExpr.args`
`ExprVec` | `Call.args`

Methods in escjava.ast with parameters of type ExprVec
`static Spec` | `Spec.make(DerivedMethodDecl dmd, ExprVec targets, ExprVec specialTargets, java.util.Hashtable preVarMap, ExprVec preAssumptions, ConditionVec pre, ExprVec postAssumptions, ConditionVec post, boolean modifiesEverything, java.util.Set postconditionLocations)`
`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 NaryExpr` | `NaryExpr.make(int sloc, int eloc, int op, Identifier methodName, ExprVec exprs)`
`static LoopCmd` | `LoopCmd.make(int locStart, int locEnd, int locHotspot, java.util.Hashtable oldmap, ConditionVec invariants, DecreasesInfoVec decreases, LocalVarDeclVec skolemConstants, ExprVec predicates, GenericVarDeclVec tempVars, GuardedCmd guard, GuardedCmd body)`
`static GeneralizedQuantifiedExpr` | `GeneralizedQuantifiedExpr.make(int sloc, int eloc, int quantifier, GenericVarDeclVec vars, Expr expr, Expr rangeExpr, ExprVec nopats)`
`static DependsPragma` | `DependsPragma.make(int tag, Expr target, ExprVec exprs, int loc)`
`static DefPredApplExpr` | `DefPredApplExpr.make(Identifier predId, ExprVec args)`
`static Call` | `Call.make(ExprVec args, int scall, int ecall, boolean inlined)`

Uses of ExprVec in escjava.pa

Fields in escjava.pa declared as ExprVec
`(package private) ExprVec` | `PredicateAbstraction.invariants`
`private ExprVec` | `PredicateAbstraction.loopPredicates`
`private ExprVec` | `GCProver.loopPredicates`

Methods in escjava.pa that return ExprVec
`static ExprVec` | `PredicateAbstraction.skolemQuantInvariants(LocalVarDeclVec skolemConstants, ExprVec invs, int sloc, int eloc)`
`(package private) ExprVec` | `GCProver.concretize(java.util.Vector clauses)`

Methods in escjava.pa with parameters of type ExprVec
`static ExprVec` | `PredicateAbstraction.skolemQuantInvariants(LocalVarDeclVec skolemConstants, ExprVec invs, int sloc, int eloc)`
`private void` | `PredicateAbstraction.guessPredicate(Expr e, Expr eOld, Type type, ExprVec predicates, int loc, Expr sca, ExprVec boundsSC)`

Constructors in escjava.pa with parameters of type ExprVec
`GCProver(mocha.wrappers.jbdd.jbddManager bddManager, ExprVec loopPredicates, GuardedCmd g, GCProver oldProver)`

Uses of ExprVec in escjava.translate

Fields in escjava.translate declared as ExprVec
`private ExprVec` | `Translate.mutexList` Used by `readCheck` and `writeCheck` to accumulate the list of mutexes protecting a shared variable.
`static ExprVec` | `TrAnExpr.trSpecExprAuxConditions`
`static ExprVec` | `TrAnExpr.trSpecExprAuxAssumptions`

Methods in escjava.translate that return ExprVec
`(package private) ExprVec` | `Translate.addNewAssumptionsNow()`
`static ExprVec` | `TrAnExpr.typeAndNonNullAllocCorrectAs(GenericVarDecl vd, Type type, SimpleModifierPragma nonNullPragma, boolean forceNonNull, java.util.Hashtable sp, boolean mentionAllocated)` Returns a vector of conjuncts.
`static ExprVec` | `TrAnExpr.getModelVarAxioms(TypeDecl td, FieldDecl fd, java.util.Hashtable sp)`
`private static ExprVec` | `GetSpec.collectAxioms(FindContributors scope)` Collects the axioms in `scope`.
`private static ExprVec` | `GetSpec.addNewAxs(java.util.HashSet axsToAdd, ExprVec assumptions)`

Methods in escjava.translate with parameters of type ExprVec
`private void` | `Translate.desugarLoopFast(LoopCmd loop, ExprVec axs)` Desugars `loop` according to the fast option.
`void` | `Translate.desugarLoopSafe(LoopCmd loop, ExprVec axs)` Desugars `loop` according to the safe option.
`private void` | `Translate.checkLoopInvariants(LoopCmd loop, ExprVec axs)` Add to "code" checks for all loop invariants of "loop".
`private void` | `Translate.addAssumptions(ExprVec ev)`
`private void` | `Translate.addNewAssumptionsNow(ExprVec ev)`
`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.
`private InlineSettings` | `Translate.computeInlineSettings(RoutineDecl rd, ExprVec argsRaw, InlineSettings inline, int scall)` Computes the inlining settings for a given call.
`static void` | `TrAnExpr.getCalledSpecs(RoutineDecl decl, ObjectDesignator od, ExprVec ev, Expr resultVar, java.util.Hashtable sp, java.util.Hashtable st)`
`private static ConditionVec` | `GetSpec.trMethodDeclPreconditions(DerivedMethodDecl dmd, ExprVec preAssumptions)` Computes the preconditions, according to section 7.2.0 of ESCJ 16.
`private static ConditionVec` | `GetSpec.trMethodDeclPostcondition(DerivedMethodDecl dmd, java.util.Hashtable wt, ExprVec postAssumptions)` Computes the postconditions, according to section 7.2.2 of ESCJ 16.
`static void` | `GetSpec.addAxioms(java.util.Set axsToAdd, ExprVec assumptions)` axsToAdd holds a Set of RepHelper - we need to add to the assumptions any axioms pertinent to the RepHelper.
`static ConditionVec` | `GetSpec.addConstraintClauses(ConditionVec post, TypeDecl decl, java.util.Hashtable wt, ExprVec postAssumptions)`
`private static ExprVec` | `GetSpec.addNewAxs(java.util.HashSet axsToAdd, ExprVec assumptions)`
`private static void` | `GetSpec.addAssumptions(ExprVec ev, StackVector code)` Appends `code` with an `assume C` command for every condition `C` in `cv`.
`static LoopCmd` | `GC.loop(int sLoop, int eLoop, int locHotspot, java.util.Hashtable oldmap, ConditionVec J, DecreasesInfoVec decs, LocalVarDeclVec skolemConsts, ExprVec P, GenericVarDeclVec tempVars, GuardedCmd B, GuardedCmd S)`
`static Expr` | `GC.nary(int tag, ExprVec ev)`
`static Expr` | `GC.nary(Identifier id, ExprVec ev)`
`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.and(ExprVec v)`
`static Expr` | `GC.and(int sloc, int eloc, ExprVec v)`
`static Expr` | `GC.or(ExprVec v)`
`static Expr` | `GC.or(int sloc, int eloc, ExprVec v)`
`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, 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 static boolean` | `GC.selectiveAdd(ExprVec to, ExprVec from, Expr bot, Expr top, int naryTagMerge)` Adds elements to `to` from `from`.
`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)'

Uses of ExprVec in javafe.ast

Fields in javafe.ast declared as ExprVec
`ExprVec` | `NewInstanceExpr.args`
`ExprVec` | `NewArrayExpr.dims` If init is null, then holds Expr's between []'s in order.
`ExprVec` | `MethodInvocation.args`
`ExprVec` | `ForStmt.forUpdate`
`ExprVec` | `ConstructorInvocation.args`
`ExprVec` | `AmbiguousMethodInvocation.args`

Methods in javafe.ast that return ExprVec
`static ExprVec` | `ExprVec.make()` * Public maker methods: * *
`static ExprVec` | `ExprVec.make(int count)`
`static ExprVec` | `ExprVec.make(java.util.Vector vec)`
`static ExprVec` | `ExprVec.make(Expr[] els)`
`static ExprVec` | `ExprVec.popFromStackVector(StackVector s)`
`ExprVec` | `ExprVec.copy()`

Methods in javafe.ast with parameters of type ExprVec
`void` | `StandardPrettyPrint.print(java.io.OutputStream o, int ind, ExprVec es)`
`abstract void` | `PrettyPrint.print(java.io.OutputStream o, int ind, ExprVec es)`
`java.lang.String` | `PrettyPrint.toString(ExprVec es)`
`static NewInstanceExpr` | `NewInstanceExpr.make(Expr enclosingInstance, int locDot, TypeName type, ExprVec args, ClassDecl anonDecl, int loc, int locOpenParen)`
`static NewArrayExpr` | `NewArrayExpr.make(Type type, ExprVec dims, ArrayInit init, int loc, int[] locOpenBrackets)`
`static MethodInvocation` | `MethodInvocation.make(ObjectDesignator od, Identifier id, TypeModifierPragmaVec tmodifiers, int locId, int locOpenParen, ExprVec args)`
`static ForStmt` | `ForStmt.make(StmtVec forInit, Expr test, ExprVec forUpdate, Stmt body, int loc, int locFirstSemi)`
`void` | `ExprVec.append(ExprVec vec)`
`void` | `DelegatingPrettyPrint.print(java.io.OutputStream o, int ind, ExprVec es)`
`static ConstructorInvocation` | `ConstructorInvocation.make(boolean superCall, Expr enclosingInstance, int locDot, int locKeyword, int locOpenParen, ExprVec args)`
`static AmbiguousMethodInvocation` | `AmbiguousMethodInvocation.make(Name name, TypeModifierPragmaVec tmodifiers, int locOpenParen, ExprVec args)`

Uses of ExprVec in javafe.parser

Methods in javafe.parser that return ExprVec
`ExprVec` | `ParseExpr.parseArgumentList(Lex l)` Parse an `ArgumentList`, which includes enclosing parens.
`ExprVec` | `ParseExpr.parseExpressionList(Lex l, int terminator)` Parse an `ExpressionList`.

Uses of ExprVec in javafe.tc

Methods in javafe.tc with parameters of type ExprVec
`protected Type[]` | `FlowInsensitiveChecks.checkExprVec(Env env, ExprVec ev)`

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 NEXT | FRAMES NO FRAMES

The ESC/Java2 Project Homepage