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
escjava.ast.ConditionVec

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

The ESC/Java2 Project Homepage