|
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 ConditionVec | |
escjava.ast | |
escjava.translate |
Uses of ConditionVec in escjava.ast |
Fields in escjava.ast declared as ConditionVec | |
ConditionVec |
Spec.pre
|
ConditionVec |
Spec.post
|
ConditionVec |
LoopCmd.invariants
|
Methods in escjava.ast that return ConditionVec | |
static ConditionVec |
ConditionVec.make()
* Public maker methods: * * |
static ConditionVec |
ConditionVec.make(int count)
|
static ConditionVec |
ConditionVec.make(java.util.Vector vec)
|
static ConditionVec |
ConditionVec.make(Condition[] els)
|
static ConditionVec |
ConditionVec.popFromStackVector(StackVector s)
|
ConditionVec |
ConditionVec.copy()
|
Methods in escjava.ast with parameters of type ConditionVec | |
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 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)
|
void |
EscPrettyPrint.printCondVec(java.io.OutputStream o,
int ind,
ConditionVec cv,
java.lang.String name)
|
void |
ConditionVec.append(ConditionVec vec)
|
Uses of ConditionVec in escjava.translate |
Methods in escjava.translate that return ConditionVec | |
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 ConditionVec |
GetSpec.addConstraintClauses(ConditionVec post,
TypeDecl decl,
java.util.Hashtable wt,
ExprVec postAssumptions)
|
Methods in escjava.translate with parameters of type ConditionVec | |
static ConditionVec |
GetSpec.addConstraintClauses(ConditionVec post,
TypeDecl decl,
java.util.Hashtable wt,
ExprVec postAssumptions)
|
private static void |
GetSpec.nonNullInitChecks(TypeDecl td,
ConditionVec post)
Add to post all NonNullInit checks for non_null instance
fields and instance ghost fields declared in td . |
private static void |
GetSpec.addFreeTypeCorrectAs(GenericVarDecl vd,
Type type,
ConditionVec cv)
Adds to cv a condition stating that vd has
type type . |
private static void |
GetSpec.assumeConditions(ConditionVec cv,
StackVector code)
|
private static void |
GetSpec.checkConditions(ConditionVec cv,
int loc,
StackVector code)
Appends code with an check loc: 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)
|
|
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 |