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
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 MethodDecls that a given class MethodDecl implements.
 Set TypeCheck.getAllImplementsSet(MethodDecl md)
          Retrieves the set of interface MethodDecls that a given class MethodDecl implements.
 Set TypeCheck.getImplementsSet(MethodDecl md)
          Retrieves the set of interface MethodDecls that a given interface MethodDecl implements.
 Set TypeCheck.getAllOverrides(MethodDecl md)
          Retrieves the set of MethodDecls 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

The ESC/Java2 Project Homepage