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.backpred.FindContributors

Packages that use FindContributors
escjava |
escjava.backpred |
escjava.gui |
escjava.translate |

Uses of FindContributors in escjava

Fields in escjava declared as FindContributors
`private static FindContributors` | `ProverManager.savedScope`

Methods in escjava with parameters of type FindContributors
`static void` | `ProverManager.push(FindContributors scope)`
`static java.util.Enumeration` | `ProverManager.prove(Expr vc, FindContributors scope)`
`int` | `Main.doProving(Expr vc, RoutineDecl r, Set directTargets, FindContributors scope)`

Uses of FindContributors in escjava.backpred

Methods in escjava.backpred with parameters of type FindContributors
`static void` | `BackPred.genTypeBackPred(FindContributors scope, java.io.PrintStream proverStream)` Return the type-specific background predicate as a formula.

Uses of FindContributors in escjava.gui

Fields in escjava.gui declared as FindContributors
`FindContributors` | `GUI.TDTreeValue.scope`

Uses of FindContributors in escjava.translate

Fields in escjava.translate declared as FindContributors
`private FindContributors` | `Translate.scope` Describes the current scope.

Methods in escjava.translate with parameters of type FindContributors
`GuardedCmd` | `Translate.trBody(RoutineDecl rd, FindContributors scope, java.util.Hashtable premap, Set predictedSynTargs, Translate inlineParent, boolean issueCautions)` Translates the body of a method or constructor, as described in ESCJ 16, section 8.
`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.
`static Spec` | `GetSpec.getSpecForCall(RoutineDecl rd, FindContributors scope, Set predictedSynTargs)`
`static Spec` | `GetSpec.getSpecForInline(RoutineDecl rd, FindContributors scope)`
`static Spec` | `GetSpec.getSpecForBody(RoutineDecl rd, FindContributors scope, Set synTargs, java.util.Hashtable premap)`
`private static Spec` | `GetSpec.getCommonSpec(RoutineDecl rd, FindContributors scope, java.util.Hashtable premap)`
`static DerivedMethodDecl` | `GetSpec.filterMethodDecl(DerivedMethodDecl dmd, FindContributors scope)`
`private static ExprModifierPragmaVec` | `GetSpec.filterExprModPragmas(ExprModifierPragmaVec vec, FindContributors scope)`
`private static ModifiesGroupPragmaVec` | `GetSpec.filterModifies(ModifiesGroupPragmaVec mvec, FindContributors scope)`
`private static VarExprModifierPragmaVec` | `GetSpec.filterVarExprModPragmas(VarExprModifierPragmaVec vec, FindContributors scope)`
`private static Spec` | `GetSpec.extendSpecForCall(Spec spec, FindContributors scope, Set predictedSynTargs)` Implements ExtendSpecForCall, section 7.3 of ESCJ 16.
`private static Spec` | `GetSpec.extendSpecForBody(Spec spec, FindContributors scope, Set synTargs)` Implements ExtendSpecForBody, section 7.4 of ESCJ 16.
`private static ExprVec` | `GetSpec.collectAxioms(FindContributors scope)` Collects the axioms in `scope`.
`private static InvariantInfo` | `GetSpec.collectInvariants(FindContributors scope, java.util.Hashtable premap)`
`private static ParamAndGlobalVarInfo` | `GetSpec.collectParamsAndGlobals(Spec spec, FindContributors scope)` Collects the parameters of `spec.args` and the static fields in `scope`, whose types are class types.
`static GuardedCmd` | `GetSpec.surroundBodyBySpec(GuardedCmd body, Spec spec, FindContributors scope, Set syntargets, java.util.Hashtable premap, int locEndCurlyBrace)` Returns a command that first does an `assume` for each precondition in `spec`, then does `body`, then checks the postconditions of `spec`, and finally checks the modifies constraints implied by `spec`.
`private static void` | `GetSpec.checkModifiesConstraints(Spec spec, FindContributors scope, Set syntargets, java.util.Hashtable premap, int loc, StackVector code)`

Constructors in escjava.translate with parameters of type FindContributors
`InitialState(FindContributors scope)`

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