|
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 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 |
||||||||||
PREV NEXT | FRAMES NO FRAMES |