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.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)
           
 


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