|
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 Set | |
escjava | |
escjava.backpred | |
escjava.pa | |
escjava.sp | |
escjava.tc | |
escjava.translate | |
javafe.tc | |
javafe.util |
Uses of Set in escjava |
Fields in escjava declared as Set | |
Set |
Options.guardVars
|
Set |
Options.ignoreAnnSet
|
Set |
Options.routinesToCheck
|
Set |
Options.routinesToSkip
|
Methods in escjava with parameters of type Set | |
int |
Main.doProving(Expr vc,
RoutineDecl r,
Set directTargets,
FindContributors scope)
|
Uses of Set in escjava.backpred |
Fields in escjava.backpred declared as Set | |
private Set |
FindContributors.visitedRoutines
The set of routines visited so far. |
private Set |
FindContributors.contributorTypes
The set of TypeSigs we've determined to be contributors so far. |
private Set |
FindContributors.contributorInvariants
The set of invariants (elementType ExprDeclPragmas) we've determined to be contributors so far. |
private Set |
FindContributors.contributorFields
The set of fields (elementType FieldDecl) we've determined to be contributors so far. |
Set |
FindContributors.preFields
|
Uses of Set in escjava.pa |
Methods in escjava.pa with parameters of type Set | |
(package private) static GuardedCmd |
Traverse.computeHelper(GuardedCmd g,
GuardedCmd context,
Set env)
|
(package private) static GuardedCmd |
PredicateAbstraction.abstractLoop(LoopCmd g,
GuardedCmd context,
Set env)
|
private GuardedCmd |
PredicateAbstraction.abstractLoopHelper(GuardedCmd context,
Set env)
|
private void |
PredicateAbstraction.inferPredicates(LoopCmd g,
Set env,
Set targets)
|
Constructors in escjava.pa with parameters of type Set | |
PredicateAbstraction(LoopCmd g,
Set env)
|
Uses of Set in escjava.sp |
Fields in escjava.sp declared as Set | |
private Set |
SPVC.cacheHit
|
Uses of Set in escjava.tc |
Methods in escjava.tc that return Set | |
static Set |
FlowInsensitiveChecks.getAllOverrides(MethodDecl md)
|
static Set |
FlowInsensitiveChecks.getDirectOverrides(MethodDecl md)
|
Methods in escjava.tc with parameters of type Set | |
static MethodDecl |
FlowInsensitiveChecks.getSuperNonNullStatus(RoutineDecl rd,
int j,
Set directOverrides)
|
Uses of Set in escjava.translate |
Fields in escjava.translate declared as Set | |
private Set |
CalcFreeVars.freeVars
|
protected Set |
VcToStringPvs.symbols
|
protected Set |
VcToStringPvs.stringLiterals
|
protected Set |
VcToString.symbols
|
protected Set |
VcToString.stringLiterals
|
private Set |
Translate.predictedSynTargs
Describes the current predicted set of synTargs. |
Set |
Translate.EverythingLoc.completed
|
(package private) Set |
Substitute.SetRef.s
|
private static Set |
LabelInfoToString.annotationLocations
set of String , each one of which has the format
filename:line:col and has been interned. |
private static Set |
LabelInfoToString.theMark
|
private static Set |
ATarget.targets
|
Methods in escjava.translate that return Set | |
(package private) Set |
CalcFreeVars.getFreeVars()
|
static Set |
Targets.normal(GuardedCmd gc)
Returns the set of normal targets of gc .
|
static Set |
Targets.direct(GuardedCmd gc)
Returns the set of variables that are direct normal targets in gc , that is, that are modified in some assignment
statement, not call statement, in gc . |
private static Set |
Suggestion.possiblyInjectiveFields(Expr e)
|
private static Set |
Suggestion.checkNaryExpr(NaryExpr e)
|
static Set |
Substitute.freeVars(ASTNode e)
Calculate the free variables of an expression or a GuardedCmd. |
static Set |
ATarget.compute(GuardedCmd gc)
|
Methods in escjava.translate with parameters of type Set | |
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. |
GuardedCmd |
Translate.modifyATargets(Set aTargets,
int loc)
targets is set of GenericVarDecls. aTargets is set of ATargets. |
GuardedCmd |
Translate.modify(Set simpleTargets,
int loc)
|
private static void |
Targets.simpleTargets(GuardedCmd gc,
Set set,
boolean includeCallTargets)
Adds SimpleTargets[[ gc ]] (as defined in ESCJ 16)
to set . |
(package private) static java.lang.String |
Suggestion.generate(int warningTag,
java.lang.Object auxInfo,
RoutineDecl rd,
Set directTargets,
SList cc,
int locDecl)
|
private static java.lang.String |
Suggestion.gNeg(VarInit E,
RoutineDecl rd,
Set directTargets)
|
static Spec |
GetSpec.getSpecForCall(RoutineDecl rd,
FindContributors scope,
Set predictedSynTargs)
|
static Spec |
GetSpec.getSpecForBody(RoutineDecl rd,
FindContributors scope,
Set synTargs,
java.util.Hashtable premap)
|
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 void |
GetSpec.addSuperInterfaces(TypeDecl td,
Set set)
|
private static void |
GetSpec.addInvariantBody(InvariantInfo ii,
Spec spec,
Set synTargs)
Extend spec , in a way appropriate for checking the body of
a method or constructor, to account for invariant ii.J
declared in class ii.U . |
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)
|
private static void |
GCSanity.checkDeclsAndUses(GuardedCmd g,
Set edci,
Set cdni,
Set euei,
Set uuei,
java.lang.String inflection,
Set sp)
Checks that there are no duplicate definitions of local variables, including implicit outermost declarations and considering dynamic inflections. |
private static void |
GCSanity.checkUses(Expr e,
Set cdni,
Set euei,
Set uuei)
|
static void |
ErrorMsg.print(java.lang.String name,
SList labelList,
SList counterexampleContext,
RoutineDecl rd,
Set directTargets,
java.io.PrintStream out)
Prints an error message for proof obligation name ,
where labelList and
counterexampleContext are labels and
counterexample from Simplify. |
private static void |
ErrorMsg.printErrorMessage(java.lang.String s,
SList counterexampleContext,
RoutineDecl rd,
Set directTargets,
java.io.PrintStream out,
boolean assocOnly)
Parses s and prints a nice error message to
out . |
static boolean |
ATarget.mentions(Expr expr,
Set s)
|
private static void |
ATarget.computeMentionsSet(ASTNode n,
Set s)
|
Uses of Set in javafe.tc |
Methods in javafe.tc that return Set | |
Set |
TypeCheck.getImplementsSet(ClassDecl cd,
MethodDecl md)
Retrieves the set of interface MethodDecl s that a given
class MethodDecl implements. |
Set |
TypeCheck.getAllImplementsSet(MethodDecl md)
Retrieves the set of interface MethodDecl s that a given
class MethodDecl implements. |
Set |
TypeCheck.getImplementsSet(MethodDecl md)
Retrieves the set of interface MethodDecl s that a
given interface MethodDecl implements. |
Set |
TypeCheck.getAllOverrides(MethodDecl md)
Retrieves the set of MethodDecl s that a given
MethodDecl overrides or hides. |
Set |
PrepTypeDeclaration.getOverrides(MethodDecl md)
Returns the set of all methods that md overrides,
where md is considered to appear in those prepped
subtypes of md.parent that inherit md .
|
Set |
PrepTypeDeclaration.getOverrides(TypeDecl td,
MethodDecl md)
Returns the set of methods that md overrides, with
md considered to appear in a particular type
td . |
Uses of Set in javafe.util |
Methods in javafe.util with parameters of type Set | |
void |
Set.intersect(Set s)
Remove all elements not contained in another set. |
boolean |
Set.union(Set s)
Adds all elements in another set. |
boolean |
Set.containsAny(Set s)
Returns whether or not the set has any element in common with 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 |
||||||||||
PREV NEXT | FRAMES NO FRAMES |