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


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