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
javafe.util.Set

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

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