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