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

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