|
ESC/Java2 © 2003,2004,2005,2006 David Cok and Joseph Kiniry © 2005,2006 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 | ||||||||||
ASTNode.
ASTDecoration object with the given
name.
ASTNode is the root of the abstract syntax tree node
hierarchy. javafe.ast. Atoms are S-expressions representing symbols. Atom representing a given
symbol.
v.
v.
v.
v.
P is "accessible".
accessibilityLowerBound !
- accessibilityLowerBound -
Variable in class escjava.tc.FlowInsensitiveChecks
-
- action -
Variable in class escjava.gui.GUI.EscTreeValue
-
- actionComplete(int, int) -
Static method in class escjava.gui.GUI
-
- actionPerformed(ActionEvent) -
Method in class escjava.gui.EscEditor
-
- actionPerformed(ActionEvent) -
Method in class escjava.gui.EscFrame.LAF
-
- actionPerformed(ActionEvent) -
Method in class escjava.gui.EscOptions.MListener
-
- actionPerformed(ActionEvent) -
Method in class escjava.gui.EscOptions
-
- actionPerformed(ActionEvent) -
Method in class escjava.gui.GuiOptionsPanel
-
- actionString(int) -
Static method in class escjava.gui.GUI
-
- activeSuffixes -
Variable in class escjava.reader.EscTypeReader
-
- actualAction(int) -
Method in class escjava.gui.GUI.EscTreeValue
-
- actualAction(int) -
Method in class escjava.gui.GUI.GFCUTreeValue
-
- actualAction(int) -
Method in class escjava.gui.GUI.IETreeValue
-
- actualAction(int) -
Method in class escjava.gui.GUI.RDTreeValue
-
- actualAction(int) -
Method in class escjava.gui.GUI.TDTreeValue
-
- add(Disjunction, DisjunctionProver) -
Method in class escjava.pa.generic.EnumNFindK
-
- add(TypeDecl, FieldDecl, Expr) -
Static method in class escjava.tc.Datagroups
- Add Expr fa to the datagroup for declaration fd in the
context of type td; the declaration fd may be in a superclass.
- add(ObjectDesignator, FieldDecl) -
Method in class escjava.translate.Frame.ModifiesIterator
- Adds the contents of the datagroup d (of object od, which
may not be null) to the 'others' list.
- add(Expr) -
Method in class escjava.translate.Translate.EverythingLoc
-
- add(Object) -
Method in class javafe.util.Set
- Add an element
Return 'true' iff the element was already in the set.
- addAllocExpression(ExprVec, Expr) -
Method in class escjava.translate.Frame
- Adds an expression into ev stating that e is allocated now but was
not allocated in the pre-state.
- addAssumption(Expr) -
Method in class escjava.translate.Translate
-
- addAssumptions(ExprVec, StackVector) -
Static method in class escjava.translate.GetSpec
- Appends
code with an assume C command for
every condition C in cv.
- addAssumptions(ExprVec) -
Method in class escjava.translate.Translate
-
- addAxioms(Set, ExprVec) -
Static method in class escjava.translate.GetSpec
- axsToAdd holds a Set of RepHelper - we need to add to the assumptions any
axioms pertinent to the RepHelper.
- addCheck(int, Condition) -
Method in class escjava.translate.Translate
- Calls
GC.check to create a check and appends the result to
code.
- addCheck(int, int, Expr) -
Method in class escjava.translate.Translate
- Calls
GC.check to create a check and appends the result to
code.
- addCheck(ASTNode, int, Expr) -
Method in class escjava.translate.Translate
- Calls
GC.check to create a check and appends the result to
code.
- addCheck(int, int, Expr, int) -
Method in class escjava.translate.Translate
- Calls
GC.check to create a check and appends the result to
code.
- addCheck(int, int, Expr, int, int) -
Method in class escjava.translate.Translate
-
- addCheck(int, int, Expr, int, Object) -
Method in class escjava.translate.Translate
- Calls
GC.check to create a check and appends the result to
code.
- addCheck(int, int, Expr, ASTNode) -
Method in class escjava.translate.Translate
- Calls
GC.check to create a check and appends the
result to code.
- addChild(String, Object) -
Method in class javafe.filespace.ExtTree
- Create a new direct child of us with label label and data newData.
- addConstraintClauses(ConditionVec, TypeDecl, Hashtable, ExprVec) -
Static method in class escjava.translate.GetSpec
-
- addContribution(TypeDecl, PrintStream) -
Static method in class escjava.backpred.BackPred
- Add to b the contribution from a particular TypeDecl, which is
a formula.
- addDefaultConstructor(TypeDeclElemVec, int, boolean) -
Method in class javafe.parser.Parse
- If no constructors are found in "elems", adds a default one to it.
- addDefaultConstructor(TypeDeclElemVec, int, boolean) -
Method in class javafe.parser.ParseExpr
- If no constructors are found in "elems", adds a default one to
it.
- addDots(String) -
Static method in class escjava.gui.EscFrame
-
- addElement(CondExprModifierPragma) -
Method in class escjava.ast.CondExprModifierPragmaVec
-
- addElement(Condition) -
Method in class escjava.ast.ConditionVec
-
- addElement(DecreasesInfo) -
Method in class escjava.ast.DecreasesInfoVec
-
- addElement(DefPred) -
Method in class escjava.ast.DefPredVec
-
- addElement(ExprDeclPragma) -
Method in class escjava.ast.ExprDeclPragmaVec
-
- addElement(ExprModifierPragma) -
Method in class escjava.ast.ExprModifierPragmaVec
-
- addElement(ExprStmtPragma) -
Method in class escjava.ast.ExprStmtPragmaVec
-
- addElement(GenericVarDecl) -
Method in class escjava.ast.GenericVarDeclVec
-
- addElement(GuardedCmd) -
Method in class escjava.ast.GuardedCmdVec
-
- addElement(LocalVarDecl) -
Method in class escjava.ast.LocalVarDeclVec
-
- addElement(CondExprModifierPragma) -
Method in class escjava.ast.ModifiesGroupPragma
-
- addElement(ModifiesGroupPragma) -
Method in class escjava.ast.ModifiesGroupPragmaVec
-
- addElement(VarExprModifierPragma) -
Method in class escjava.ast.VarExprModifierPragmaVec
-
- addElement(CatchClause) -
Method in class javafe.ast.CatchClauseVec
-
- addElement(Expr) -
Method in class javafe.ast.ExprVec
-
- addElement(FieldDecl) -
Method in class javafe.ast.FieldDeclVec
-
- addElement(FormalParaDecl) -
Method in class javafe.ast.FormalParaDeclVec
-
- addElement(Identifier) -
Method in class javafe.ast.IdentifierVec
-
- addElement(ImportDecl) -
Method in class javafe.ast.ImportDeclVec
-
- addElement(LexicalPragma) -
Method in class javafe.ast.LexicalPragmaVec
-
- addElement(MethodDecl) -
Method in class javafe.ast.MethodDeclVec
-
- addElement(ModifierPragma) -
Method in class javafe.ast.ModifierPragmaVec
-
- addElement(Stmt) -
Method in class javafe.ast.StmtVec
-
- addElement(TypeDeclElem) -
Method in class javafe.ast.TypeDeclElemVec
-
- addElement(TypeDecl) -
Method in class javafe.ast.TypeDeclVec
-
- addElement(TypeModifierPragma) -
Method in class javafe.ast.TypeModifierPragmaVec
-
- addElement(TypeName) -
Method in class javafe.ast.TypeNameVec
-
- addElement(VarInit) -
Method in class javafe.ast.VarInitVec
-
- addElement(TypeSig) -
Method in class javafe.tc.TypeSigVec
-
- addElement(Object) -
Method in class javafe.util.StackVector
- Add an element at the end of the top Vector.
- addElementInternal(Object) -
Method in class javafe.util.StackVector
- Add x to the end of the top Vector.
- addEnd(SExp) -
Method in class escjava.prover.SList
-
- addEnumeration(Enumeration) -
Method in class javafe.util.Set
- Add all the elements of a given enumeration
- addField(FieldDecl) -
Method in class escjava.backpred.FindContributors
- Add a given field to contributorFields, maintaining all the
closure properties.
- addFields(ObjectDesignator) -
Method in class escjava.translate.Frame.ModifiesIterator
- Adds all the fields of the od (whether it is a type
or an object) into the 'others' list as FieldAccess
items.
- addFreeTypeCorrectAs(GenericVarDecl, Type, ConditionVec) -
Static method in class escjava.translate.GetSpec
- Adds to
cv a condition stating that vd has
type type.
- addFront(SExp) -
Method in class escjava.prover.SList
-
- addImplicitConstructorRefs(ConstructorDecl, FieldDeclVec, boolean, LinkedList) -
Method in class escjava.backpred.FindContributors
- Add implicit references from a ConstructorDecl that do not
appear in Java code or via backedges as per walk(,,).
- addInheritedMembers(TypeSig, TypeSig) -
Method in class escjava.tc.PrepTypeDeclaration
-
- addInheritedMembers(TypeSig, TypeSig) -
Method in class javafe.tc.PrepTypeDeclaration
- Find all members of a supertype inherited by a type.
- addInheritedSpecs(RoutineDecl, ModifierPragmaVec) -
Static method in class escjava.ast.Utils
-
- addInvariant(ExprDeclPragma) -
Method in class escjava.backpred.FindContributors
- Add a given invariant to contributorInvarints, maintaining all
closure properties.
- addInvariantBody(InvariantInfo, Spec, Set) -
Static method in class escjava.translate.GetSpec
- 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.
- addJavaKeywords() -
Method in class javafe.parser.Lex
- Add all of Java's keywords to the scanner.
- addJavaPunctuation() -
Method in class javafe.parser.Lex
- Add all of Java's punctuation strings to the scanner.
- addKeyword(String, int) -
Method in class javafe.parser.Lex
- Add a keyword to a
Lex object with the given code.
- addLoopDecreases(LoopCmd, int) -
Method in class escjava.translate.Translate
- Adds to
code the various pieces of the translation of the
decreases pragma.
- addMapping(GenericVarDecl) -
Method in class escjava.translate.InitialState
-
- addModifiersToDMD(DerivedMethodDecl, RoutineDecl) -
Static method in class escjava.translate.GetSpec
- * Add the modifiers of rd to dmd, making any necessary substitions * of
parameter names.
- addMoreLocations(Set) -
Method in class escjava.translate.Translate
-
- addName(String, String, String) -
Static method in class escjava.vcGeneration.TNode
- This function add variable to the global map name.
- addName(String, String) -
Static method in class escjava.vcGeneration.TNode
-
- addNewAssumptions() -
Method in class escjava.translate.Translate
-
- addNewAssumptionsHelper() -
Method in class escjava.translate.Translate
-
- addNewAssumptionsNow() -
Method in class escjava.translate.Translate
-
- addNewAssumptionsNow(ExprVec) -
Method in class escjava.translate.Translate
-
- addNewAxs(HashSet, ExprVec) -
Static method in class escjava.translate.GetSpec
-
- addNewString(VarInit, Expr, Expr) -
Method in class escjava.translate.Translate
-
- addNonSyntheticDecls(TypeDeclElemVec, TypeDeclElem[]) -
Method in class javafe.reader.ASTClassFileParser
- Add only AST nodes that are not synthetic decls to v.
- addOperator(int, int, boolean) -
Method in class javafe.parser.ParseExpr
- Add an infix, binary operator to the parser with a given
precedence and associativity.
- addOverride(MethodDecl, MethodDecl) -
Method in class javafe.tc.PrepTypeDeclaration
- Decorates MethodDecl of prepped TypeDecls with a Set of
methods that decl overrides or hides.
- addPath(String[]) -
Method in class javafe.filespace.ExtTree
- This is an extended version of addChild that takes a path (a
list of labels) instead of a single label.
- addPerfCounters(GCProver) -
Method in class escjava.pa.GCProver
-
- addPossibleInvariant(ExprDeclPragma) -
Method in class escjava.backpred.FindContributors
- Add a possible invariant contributor to either fieldToPossible
or contributorInvariants as approperiate, maintaining all
closure properties.
- addPossibleMentions(FieldDecl, ExprDeclPragma) -
Method in class escjava.backpred.FindContributors
- Add the mapping (fd, J) to fieldToPossible.
- addPunctuation(String, int) -
Method in class javafe.parser.Lex
- Add a punctuation string to a scanner associated with a given
code.
- addRelAsgCast(Expr, Type, Type) -
Static method in class escjava.translate.Translate
-
- addSon(TNode) -
Method in class escjava.vcGeneration.TFunction
-
- addSource(GenericFile) -
Static method in class javafe.tc.OutsideEnv
- Attempt to add the package-member types contained in a source
file to the package-member-types environment, returning the
CompilationUnit, if any, found in that file.
- addSource(String) -
Static method in class javafe.tc.OutsideEnv
- Attempt to add the package-member types contained in a named
source file to the package-member-types environment, returning
the
CompilationUnit, if any, found in that
file.
- addSources(ArrayList) -
Static method in class javafe.tc.OutsideEnv
- Adds all relevant files from the given package; 'relevant' is
defined by the 'findFiles' method of the current reader.
- addStmt(Lex) -
Method in class escjava.parser.EscPragmaParser
-
- addStmt(Lex) -
Method in class javafe.parser.ParseStmt
- Internal method for parsing a
Stmt.
- addSuperInterfaces(TypeDecl, Set) -
Static method in class escjava.translate.GetSpec
-
- addTarget(GenericVarDecl) -
Static method in class escjava.translate.ATarget
-
- addTarget(GenericVarDecl, Expr) -
Static method in class escjava.translate.ATarget
-
- addTarget(GenericVarDecl, Expr, Expr) -
Static method in class escjava.translate.ATarget
-
- addTarget(GenericVarDecl, Expr[]) -
Static method in class escjava.translate.ATarget
-
- addTask(Object) -
Method in class escjava.gui.TaskQueue
-
- addTask(Object) -
Static method in class escjava.gui.WindowTasks
-
- addToMap(Map, Map) -
Static method in class escjava.tc.Datagroups
-
- addTraceLabelSequenceNumbers(GuardedCmd) -
Static method in class escjava.translate.Translate
- Destructively change the trace labels in
gc to insert sequence
numbers that are used by the ErrorMsg class in printing trace labels in the
correct execution order.
- addType(Type) -
Method in class escjava.backpred.FindContributors
- Add the TypeSigs mentioned explicitly in a given Type to
contributorTypes, maintaining all the closure properties.
- addType(String, String) -
Static method in class escjava.vcGeneration.TNode
- This function add type to the global map .
- addType(String) -
Static method in class escjava.vcGeneration.TNode
-
- addTypeInfo(InitialState, Expr) -
Method in class escjava.vcGeneration.ProverType
- This method is used by untyped prover logics to add typing predicates to
the supplied VC term.
- addTypeInfo(InitialState, Expr) -
Method in class escjava.vcGeneration.coq.CoqProver
-
- addTypeInfo(InitialState, Expr) -
Method in class escjava.vcGeneration.pvs.PvsProver
-
- addTypeInfo(InitialState, Expr) -
Method in class escjava.vcGeneration.sammy.SammyProver
-
- addTypeInfo(InitialState, Expr) -
Method in class escjava.vcGeneration.simplify.SimplifyProver
-
- addTypeInfo(InitialState, Expr) -
Method in class escjava.vcGeneration.xml.XmlProver
- At this stage, we do not know if the target prover is typed or not.
- addVarDeclStmts(Lex, int, ModifierPragmaVec, Type) -
Method in class javafe.parser.ParseStmt
- Internal routine for parsing variable declarations
after the leading type has been parsed.
- addZipEntry(ZipEntry) -
Method in class javafe.filespace.ZipTree
- Add a ZipEntry to this tree according to its pathname:
- adorn(VariableAccess) -
Method in class escjava.translate.Translate
- Make a fresh version of a special variable to save it in.
- allCorrStreams -
Static variable in class javafe.util.LocationManagerCorrelatedReader
- A static Vector containing all LocationManagerCorrelatedReader
instances, in the order they were allocated, which is used to
map a given location to a corresponding LocationManagerCorrelatedReader
instance.
- allInvalidClauses -
Variable in class escjava.pa.GCProver
-
- allSpecs -
Static variable in class escjava.ast.Utils
-
- allocUseOpt -
Variable in class escjava.Options
-
- allocated -
Static variable in class javafe.ast.ASTDecoration
- *
Class variables: *
*
- allocatesDecoration -
Static variable in class escjava.ast.Utils
-
- allocvar -
Static variable in class escjava.translate.GC
-
- allowAlsoRequires -
Variable in class escjava.Options
-
- allowAvoidSpec -
Static variable in class javafe.SrcToolOptions
- Do we allow the
-avoidSpec option?
- allowDepend -
Static variable in class javafe.SrcToolOptions
- Do we allow the -depend option?
- allowSpecialSuffix -
Variable in class escjava.parser.JmlCorrelatedReader
- Indicates whether or not a sequence of consecutive special
characters at the end of the comment are to be treated as white
space.
- allowedExceptions -
Variable in class javafe.tc.FlowInsensitiveChecks
-
- ambiguousPackage -
Variable in class javafe.filespace.Resolve_AmbiguousName
-
- and(Expr, Expr) -
Static method in class escjava.AnnotationHandler
- Produces an expression which is the conjunction of the two expressions.
- and(ExprModifierPragma, ExprModifierPragma) -
Static method in class escjava.AnnotationHandler
- Produces an ExprModifierPragma whose expression is the conjunction of the
expressions in the input pragmas.
- and(ArrayList) -
Static method in class escjava.AnnotationHandler
- Produces an ExprModifierPragma whose expression is the conjunction of all
of the expressions in the ExprModifierPragmas in the argument.
- and(Expr, Expr) -
Static method in class escjava.translate.GC
-
- and(int, int, Expr, Expr) -
Static method in class escjava.translate.GC
-
- and(ExprVec) -
Static method in class escjava.translate.GC
-
- and(int, int, ExprVec) -
Static method in class escjava.translate.GC
-
- andLabeled(ArrayList) -
Static method in class escjava.AnnotationHandler
- The same as and(ArrayList), but produces labelled expressions within the
conjunction so that error messages come out with useful locations.
- andx(Expr, Expr) -
Static method in class escjava.translate.GC
-
- annotationHandler -
Variable in class escjava.Main
-
- annotationHandler -
Variable in class escjava.reader.RefinementCachedReader
- The underlying Reader whose results we are caching.
- annotationHandler -
Variable in class escjava.tc.FlowInsensitiveChecks
-
- annotationLocations -
Static variable in class escjava.translate.LabelInfoToString
- set of
String, each one of which has the format
filename:line:col and has been interned.
- anonDecl -
Variable in class javafe.ast.NewInstanceExpr
- If the new expression includes a declaration of an inner class,
then "anonDecl" will be non-null.
- anyType -
Static variable in class escjava.tc.Types
-
- append(CondExprModifierPragmaVec) -
Method in class escjava.ast.CondExprModifierPragmaVec
-
- append(ConditionVec) -
Method in class escjava.ast.ConditionVec
-
- append(DecreasesInfoVec) -
Method in class escjava.ast.DecreasesInfoVec
-
- append(DefPredVec) -
Method in class escjava.ast.DefPredVec
-
- append(ExprDeclPragmaVec) -
Method in class escjava.ast.ExprDeclPragmaVec
-
- append(ExprModifierPragmaVec) -
Method in class escjava.ast.ExprModifierPragmaVec
-
- append(ExprStmtPragmaVec) -
Method in class escjava.ast.ExprStmtPragmaVec
-
- append(GenericVarDeclVec) -
Method in class escjava.ast.GenericVarDeclVec
-
- append(GuardedCmdVec) -
Method in class escjava.ast.GuardedCmdVec
-
- append(LocalVarDeclVec) -
Method in class escjava.ast.LocalVarDeclVec
-
- append(ModifiesGroupPragma) -
Method in class escjava.ast.ModifiesGroupPragma
-
- append(CondExprModifierPragmaVec) -
Method in class escjava.ast.ModifiesGroupPragma
-
- append(ModifiesGroupPragmaVec) -
Method in class escjava.ast.ModifiesGroupPragmaVec
-
- append(VarExprModifierPragmaVec) -
Method in class escjava.ast.VarExprModifierPragmaVec
-
- append(SList) -
Method in class escjava.prover.SList
-
- append(String) -
Method in class escjava.vcGeneration.PrettyPrinter
- append indentation and parameter
- append(CatchClauseVec) -
Method in class javafe.ast.CatchClauseVec
-
- append(ExprVec) -
Method in class javafe.ast.ExprVec
-
- append(FieldDeclVec) -
Method in class javafe.ast.FieldDeclVec
-
- append(FormalParaDeclVec) -
Method in class javafe.ast.FormalParaDeclVec
-
- append(IdentifierVec) -
Method in class javafe.ast.IdentifierVec
-
- append(ImportDeclVec) -
Method in class javafe.ast.ImportDeclVec
-
- append(LexicalPragmaVec) -
Method in class javafe.ast.LexicalPragmaVec
-
- append(MethodDeclVec) -
Method in class javafe.ast.MethodDeclVec
-
- append(ModifierPragmaVec) -
Method in class javafe.ast.ModifierPragmaVec
-
- append(StmtVec) -
Method in class javafe.ast.StmtVec
-
- append(TypeDeclElemVec) -
Method in class javafe.ast.TypeDeclElemVec
-
- append(TypeDeclVec) -
Method in class javafe.ast.TypeDeclVec
-
- append(TypeModifierPragmaVec) -
Method in class javafe.ast.TypeModifierPragmaVec
-
- append(TypeNameVec) -
Method in class javafe.ast.TypeNameVec
-
- append(VarInitVec) -
Method in class javafe.ast.VarInitVec
-
- append(int) -
Method in class javafe.parser.Lex
- Append 'c' to
text, expanding if necessary.
- append(TypeSigVec) -
Method in class javafe.tc.TypeSigVec
-
- appendI(String) -
Method in class escjava.vcGeneration.PrettyPrinter
- This function goes to next line, increases indentation by two spaces
and add a '('
If you want to change the indentation style do it here.
- appendIwNl(String) -
Method in class escjava.vcGeneration.PrettyPrinter
- This function increases indentation by two spaces
and add a '('
If you want to change the indentation style do it here.
- appendN(String) -
Method in class escjava.vcGeneration.PrettyPrinter
- just append the parameter, N stands for normal
- appendParameter(Type) -
Method in class javafe.reader.MethodSignature
- Append a parameter type to this method signature.
- appendText(String) -
Method in class escjava.gui.EscOutputFrame
- Appends text to that already contained in the frame.
- apply(Expr) -
Method in class escjava.sp.VarMap
- Returns the result of applying "this", viewed as a
substituiton, to "e".
- apply(Hashtable, VariableAccess) -
Static method in class escjava.translate.TrAnExpr
-
- applyEnv(Hashtable, Expr) -
Static method in class escjava.translate.ATarget
- Returns null if expr not loop constant
- areDifferent() -
Method in class junitutils.Diff
- Returns true if strings on which this was constructed are different.
- arg -
Variable in class escjava.ast.VarExprModifierPragma
-
- arg -
Variable in class javafe.ast.CatchClause
-
- argListInAnnotation -
Variable in class escjava.parser.EscPragmaParser
-
- argTypes -
Variable in class escjava.vcGeneration.TMethodCall
-
- argTypes() -
Method in class javafe.ast.RoutineDecl
-
- args -
Variable in class escjava.ast.Call
-
- args -
Variable in class escjava.ast.DefPred
-
- args -
Variable in class escjava.ast.DefPredApplExpr
-
- args -
Variable in class escjava.ast.DerivedMethodDecl
-
- args -
Variable in class javafe.ast.AmbiguousMethodInvocation
-
- args -
Variable in class javafe.ast.ConstructorInvocation
-
- args -
Variable in class javafe.ast.MethodInvocation
-
- args -
Variable in class javafe.ast.NewInstanceExpr
-
- args -
Variable in class javafe.ast.RoutineDecl
-
- args -
Variable in class junitutils.TestFilesTestSuite.Helper
- Command-line arguments (including filename) for this test.
- argtypes -
Variable in class javafe.ast.RoutineDecl
-
- array -
Variable in class escjava.ast.ArrayRangeRefExpr
-
- array -
Variable in class javafe.ast.ArrayRefExpr
-
- arrayAccessCheck(Expr, Expr, Expr, Expr, int) -
Method in class escjava.translate.Translate
- Emit the checks that
array is non-null and that
index is inbounds for array.
- arrayToString(Object[], String) -
Static method in class javafe.parser.ParseUtil
-
- asStaticContext() -
Method in class escjava.tc.EnvForGhostLocals
- Returns a new Env that acts the same as us, except that its
current instance (if any) is not accessible.
- asStaticContext() -
Method in class escjava.tc.GhostEnv
- Returns a new
Env that acts the same as us, except that its current
instance (if any) is not accessible.
- asStaticContext() -
Method in class javafe.tc.Env
- Returns a new Env that acts the same as us, except that its
current instance (if any) is not accessible.
- asStaticContext() -
Method in class javafe.tc.EnvForCU
- Returns a new Env that acts the same as us, except that its
current instance (if any) is not accessible.
- asStaticContext() -
Method in class javafe.tc.EnvForEnclosedScope
- Returns a new Env that acts the same as us, except that its
current instance (if any) is not accessible.
- asStaticContext() -
Method in class javafe.tc.EnvForLocalType
- Returns a new Env that acts the same as us, except that its
current instance (if any) is not accessible.
- asStaticContext() -
Method in class javafe.tc.EnvForLocals
- Returns a new Env that acts the same as us, except that its
current instance (if any) is not accessible.
- asStaticContext() -
Method in class javafe.tc.EnvForTypeSig
- Returns a new Env that acts the same as us, except that its
current instance (if any) is not accessible.
- assertContinue -
Variable in class escjava.Options
-
- assertContinueCounter -
Static variable in class escjava.translate.GC
-
- assertDiff(String, String) -
Method in class junitutils.TestCase
-
- assertEquals(String, String, boolean) -
Method in class junitutils.TestCase
- Compare Strings for equality with better difference reporting.
- assertIsKeyword -
Variable in class javafe.Options
- Are we parsing Java 1.4 source code (i.e., we must parse the
new "assert" Java keyword).
- assertPredicate(int, int, Expr, int, int, Object) -
Static method in class escjava.translate.GC
-
- assertionMode -
Variable in class escjava.Options
-
- assertionsEnabled -
Variable in class javafe.Options
- Java allows assertions to be enabled and disabled.
- assignmentConvertable(Expr, Type) -
Method in class escjava.tc.FlowInsensitiveChecks
-
- assignmentConvertable(Expr, Type) -
Method in class javafe.tc.FlowInsensitiveChecks
- Checks if Exp e can be assigned to Type t.
- assocDeclClipPolicy -
Static variable in class escjava.translate.ErrorMsg
-
- assocLoc(int) -
Static method in class javafe.util.ErrorSet
-
- assume(Expr) -
Static method in class escjava.translate.GC
-
- assumeAnnotation(int, Expr) -
Static method in class escjava.translate.GC
-
- assumeCondition(Expr, int) -
Static method in class escjava.translate.GC
-
- assumeConditions(ConditionVec, StackVector) -
Static method in class escjava.translate.GetSpec
-
- assumeNegation(Expr) -
Static method in class escjava.translate.GC
-
- at(int) -
Method in class escjava.prover.SList
-
- atStartOfConstructorOrMethod(Lex) -
Method in class javafe.parser.Parse
- checks for X TypeModifierPragma* (
in the input stream.
- auto -
Variable in class javafe.InputEntry
-
- autoBoundVariable -
Static variable in class escjava.translate.UniqName
- Use this location *only* in declarations of automatically
generated bound variables.
- autoExpand -
Variable in class escjava.gui.GuiOptionsPanel.Settings
-
- autoScroll -
Variable in class escjava.gui.GuiOptionsPanel.Settings
-
- autoShowErrors -
Variable in class escjava.gui.GuiOptionsPanel.Settings
-
- auxVal -
Variable in class javafe.parser.Token
- Auxillary information about the token.
- auxval -
Variable in class escjava.parser.EscPragmaParser.SavedPragma
-
- avoidSpec -
Variable in class javafe.SrcToolOptions
- Should we avoid specs for all types loaded after the initial
set of source files?
- avoidSpec -
Static variable in class javafe.tc.OutsideEnv
- When we load in types, do we prefer to read specs or non-specs?
- axiomDecoration -
Static variable in class escjava.ast.Utils
-
- axsToAdd -
Static variable in class escjava.translate.Translate
-
CorrelatedReader contain a buffer.buf as null.
s, call them a
and b.
BranchStmt nodes to point to labelled Stmt
objects.
buf, which
grows on demand.
exp using Simplify process
simplify.
CompilationUnit-level type
checks.
make method of this class has the side effect of
pointing the parent pointers of the TypeDecls
inside a CompilationUnit to point to that unit.ProverType.
TypeCheck.canAccess(javafe.tc.TypeSig, javafe.tc.TypeSig, int, javafe.ast.ModifierPragmaVec) to account for
spec_public.
Identifier
created.
null).
check above.
check above.
CompilationUnit.
code with an check loc: C command for
every condition C in cv.
fd into implementation checked state.
CompilationUnit to make sure that each import is
individually well formed.
- checkIncDecExpr(Env, UnaryExpr) -
Method in class javafe.tc.FlowInsensitiveChecks
- Typecheck unary increment and decrement operators (e.g., ++x).
- checkInit(Env, VarInit, Type) -
Method in class javafe.tc.FlowInsensitiveChecks
-
- checkInstanceOfExpr(Env, InstanceOfExpr) -
Method in class javafe.tc.FlowInsensitiveChecks
- Typechecks a dynamic type probe (e.g., x instanceof X).
- checkIntLitExpr(Expr) -
Method in class javafe.tc.FlowInsensitiveChecks
- Typechecks integers (e.g., 29).
- checkIntegralType(Expr) -
Static method in class javafe.tc.FlowInsensitiveChecks
-
- checkLongLitExpr(Expr) -
Method in class javafe.tc.FlowInsensitiveChecks
- Typechecks long literal expressions (e.g., 29L).
- checkLoopDecreases(Env, boolean) -
Method in class escjava.tc.FlowInsensitiveChecks
-
- checkLoopInvariants(Env, boolean) -
Method in class escjava.tc.FlowInsensitiveChecks
-
- checkLoopInvariants(LoopCmd, ExprVec) -
Method in class escjava.translate.Translate
- Add to "code" checks for all loop invariants of "loop".
- checkLoopPredicates(Env, boolean) -
Method in class escjava.tc.FlowInsensitiveChecks
-
- checkMaybeAdd(Expr, TypeNameVec, int) -
Method in class escjava.AnnotationHandler
-
- checkMethodInvocationExpr(Env, MethodInvocation) -
Method in class javafe.tc.FlowInsensitiveChecks
- Typecheck method invocation.
- checkModifierPragma(ModifierPragma, ASTNode, Env) -
Method in class escjava.tc.FlowInsensitiveChecks
-
- checkModifierPragma(ModifierPragma, ASTNode, Env) -
Method in class javafe.tc.FlowInsensitiveChecks
- Hook to do additional processing on
Modifiers.
- checkModifierPragmaVec(ModifierPragmaVec, ASTNode, Env) -
Method in class javafe.tc.FlowInsensitiveChecks
- Hook to do additional processing on
ModifierVecs.
- checkModifiers(int, int, int, String) -
Method in class javafe.tc.PrepTypeDeclaration
-
- checkModifiesConstraints(Spec, FindContributors, Set, Hashtable, int, StackVector) -
Static method in class escjava.translate.GetSpec
-
- checkMoreArguments(String, String[], int) -
Method in class javafe.Options
-
- checkNaryExpr(NaryExpr) -
Static method in class escjava.translate.Suggestion
-
- checkNewArrayExpr(Env, NewArrayExpr) -
Method in class javafe.tc.FlowInsensitiveChecks
- Typecheck a new array construction (e.g., new int[100]).
- checkNewInstanceExpr(Env, NewInstanceExpr) -
Method in class javafe.tc.FlowInsensitiveChecks
- Typecheck a class instantiation (e.g., new C()).
- checkNoModifiers(int, int) -
Method in class escjava.parser.EscPragmaParser
- Issues an error if any Java modifiers have accumulated, and resets the
accumulated modifiers to NONE.
- checkNoRepInStaticContext(ASTNode) -
Method in class javafe.tc.FlowInsensitiveChecks
-
- checkNotExpr(Env, UnaryExpr) -
Method in class javafe.tc.FlowInsensitiveChecks
- Typecheck boolean not (e.g., !
- checkNullLitExpr(Expr) -
Method in class javafe.tc.FlowInsensitiveChecks
- Typechecks null.
- checkNumericType(Expr) -
Static method in class javafe.tc.FlowInsensitiveChecks
-
- checkObjectDesignator(TypeSig, ObjectDesignator) -
Static method in class javafe.tc.CheckInvariants
-
- checkObjectDesignator(Env, ObjectDesignator) -
Method in class javafe.tc.FlowInsensitiveChecks
-
- checkParenExpr(Env, ParenExpr) -
Method in class javafe.tc.FlowInsensitiveChecks
- Typechecks paranthesis.
- checkPredicate(Env, Expr) -
Method in class escjava.tc.FlowInsensitiveChecks
-
- checkPublic(CompilationUnit) -
Static method in class javafe.tc.CheckCompilationUnit
- Check a
CompilationUnit to make sure that the only type that may
be declared public in it is the one with the same name as the file it occurs
in.
- checkPurity -
Variable in class escjava.Options
- Temporary option to turn on purity checking, since it is off by
default until purity issues with inheritance are resolved.
- checkRedundantSpecs -
Variable in class escjava.Options
- Statically check against redundant specs?
- checkReturnValue(String, String, Object) -
Method in class junitutils.TestFilesTestSuite
-
- checkSignExpr(Env, UnaryExpr) -
Method in class javafe.tc.FlowInsensitiveChecks
- Typecheck sign (e.g.
- checkSignalsOnly(ModifierPragmaVec, RoutineDecl) -
Method in class escjava.AnnotationHandler
-
- checkSkolemConstants(Env, boolean) -
Method in class escjava.tc.FlowInsensitiveChecks
-
- checkSpecs -
Variable in class escjava.Options
-
- checkStmt(Env, Stmt) -
Method in class escjava.tc.FlowInsensitiveChecks
-
- checkStmt(TypeSig, Stmt) -
Static method in class javafe.tc.CheckInvariants
-
- checkStmt(Env, Stmt) -
Method in class javafe.tc.FlowInsensitiveChecks
- Typecheck a statement in a given environment then return the environment
in effect for statements that follow the given statement.
- checkStmtPragma(Env, StmtPragma) -
Method in class escjava.tc.FlowInsensitiveChecks
-
- checkStmtPragma(Env, StmtPragma) -
Method in class javafe.tc.FlowInsensitiveChecks
-
- checkStmtVec(Env, StmtVec) -
Method in class javafe.tc.FlowInsensitiveChecks
-
- checkString(String) -
Method in class escjava.prover.SubProcess
- Ensure that the next output characters from this subprocess
(consumed in the process) matches the provided string.
- checkStringLitExpr(Expr) -
Method in class javafe.tc.FlowInsensitiveChecks
- Typechecks strings.
- checkSuperInterfaces(TypeSig, TypeNameVec) -
Method in class escjava.tc.PrepTypeDeclaration
-
- checkSuperInterfaces(TypeSig, TypeNameVec) -
Method in class javafe.tc.PrepTypeDeclaration
- Check superinterfaces
and add their members to fieldSeq and methodSeq.
- checkSuperTypeAccessible(TypeSig, TypeSig, int) -
Method in class javafe.tc.PrepTypeDeclaration
- Check to make sure a supertype is accessible; reports an error
to ErrorSet if not.
- checkSwitchStmt(Env, SwitchStmt) -
Method in class javafe.tc.FlowInsensitiveChecks
-
- checkTag(int) -
Method in class escjava.parser.ErrorPragmaParser
- We consider both ESC and Javadoc comments to be annotations.
- checkTag(int) -
Method in class escjava.parser.EscPragmaParser
-
- checkTag(int) -
Method in interface javafe.parser.PragmaParser
- Decide whether a comment contains pragmas.
- checkThisExpr(Env, ThisExpr) -
Method in class javafe.tc.FlowInsensitiveChecks
- Typechecks this expression.
- checkType(Type, boolean) -
Static method in class javafe.tc.CheckInvariants
-
- checkType(Expr, Type) -
Static method in class javafe.tc.FlowInsensitiveChecks
-
- checkTypeDecl(TypeDecl) -
Method in class javafe.tc.TypeCheck
- Moves
td into the checked state.
- checkTypeDeclElem(TypeDeclElem) -
Method in class escjava.tc.FlowInsensitiveChecks
-
- checkTypeDeclElem(TypeDeclElem) -
Method in class javafe.tc.FlowInsensitiveChecks
-
- checkTypeDeclElemPragma(TypeDeclElemPragma) -
Method in class escjava.tc.FlowInsensitiveChecks
-
- checkTypeDeclElemPragma(TypeDeclElemPragma) -
Method in class javafe.tc.FlowInsensitiveChecks
-
- checkTypeDeclOfSig(TypeSig) -
Static method in class javafe.tc.CheckInvariants
-
- checkTypeDeclaration(TypeSig) -
Method in class escjava.tc.FlowInsensitiveChecks
-
- checkTypeDeclaration(TypeSig) -
Method in class javafe.tc.FlowInsensitiveChecks
- Moves
s into implementation checked state.
- checkTypeModifierPragma(TypeModifierPragma, ASTNode, Env) -
Method in class javafe.tc.FlowInsensitiveChecks
-
- checkTypeModifierPragmaVec(TypeModifierPragmaVec, ASTNode, Env) -
Method in class javafe.tc.FlowInsensitiveChecks
-
- checkTypeModifiers(Env, Type) -
Method in class javafe.tc.FlowInsensitiveChecks
- This may be called more than once on a Type t.
- checkTypeModifiers(TypeDecl, TypeSig, boolean) -
Method in class javafe.tc.PrepTypeDeclaration
- Check that the modifiers of a type are ok.
- checkTypeSig(TypeSig) -
Method in class javafe.tc.TypeCheck
- Moves
s into the checked state.
- checkUniverseAssignability(ASTNode, ASTNode) -
Static method in class javafe.tc.FlowInsensitiveChecks
- Tests if universe modifiers of
r can be
assigned to l.
- checkUniverseCastability(ASTNode, ASTNode) -
Static method in class javafe.tc.FlowInsensitiveChecks
- Tests if the cast of the universe modifiers
l
r is ever possible.
- checkUniverseForField(GenericVarDecl) -
Method in class javafe.tc.FlowInsensitiveChecks
-
- checkUses(Expr, Set, Set, Set) -
Static method in class escjava.translate.GCSanity
-
- checkVarDeclStmt(Env, LocalVarDecl) -
Method in class javafe.tc.FlowInsensitiveChecks
-
- checkVariableAccessExpr(VariableAccess) -
Method in class javafe.tc.FlowInsensitiveChecks
- Typecheck variable access.
- checkedField -
Static variable in class javafe.tc.CheckCompilationUnit
- A new field for CompilationUnits: iff it is non-null then we have already
checked that CompilationUnit.
- checks -
Variable in class escjava.ast.NowarnPragma
-
- child -
Variable in class javafe.util.FilterCorrelatedReader
-
- childAt(int) -
Method in class escjava.ast.AnOverview
- Return the first-but-ith child of a node.
- childAt(int) -
Method in class escjava.ast.ArrayRangeRefExpr
-
- childAt(int) -
Method in class escjava.ast.Call
-
- childAt(int) -
Method in class escjava.ast.CmdCmdCmd
-
- childAt(int) -
Method in class escjava.ast.CondExprModifierPragma
-
- childAt(int) -
Method in class escjava.ast.Condition
-
- childAt(int) -
Method in class escjava.ast.DecreasesInfo
-
- childAt(int) -
Method in class escjava.ast.DefPred
-
- childAt(int) -
Method in class escjava.ast.DefPredApplExpr
-
- childAt(int) -
Method in class escjava.ast.DefPredLetExpr
-
- childAt(int) -
Method in class escjava.ast.DependsPragma
-
- childAt(int) -
Method in class escjava.ast.DynInstCmd
-
- childAt(int) -
Method in class escjava.ast.EscPrimitiveType
-
- childAt(int) -
Method in class escjava.ast.EverythingExpr
-
- childAt(int) -
Method in class escjava.ast.ExprCmd
-
- childAt(int) -
Method in class escjava.ast.ExprDeclPragma
-
- childAt(int) -
Method in class escjava.ast.ExprModifierPragma
-
- childAt(int) -
Method in class escjava.ast.ExprStmtPragma
-
- childAt(int) -
Method in class escjava.ast.GCExpr
- Return the first-but-ith child of a node.
- childAt(int) -
Method in class escjava.ast.GeneralizedQuantifiedExpr
-
- childAt(int) -
Method in class escjava.ast.GetsCmd
-
- childAt(int) -
Method in class escjava.ast.GhostDeclPragma
-
- childAt(int) -
Method in class escjava.ast.GuardExpr
-
- childAt(int) -
Method in class escjava.ast.GuardedCmd
- Return the first-but-ith child of a node.
- childAt(int) -
Method in class escjava.ast.IdExprDeclPragma
-
- childAt(int) -
Method in class escjava.ast.IdentifierModifierPragma
-
- childAt(int) -
Method in class escjava.ast.ImportPragma
-
- childAt(int) -
Method in class escjava.ast.LabelExpr
-
- childAt(int) -
Method in class escjava.ast.LockSetExpr
-
- childAt(int) -
Method in class escjava.ast.LoopCmd
-
- childAt(int) -
Method in class escjava.ast.MapsExprModifierPragma
-
- childAt(int) -
Method in class escjava.ast.ModelConstructorDeclPragma
-
- childAt(int) -
Method in class escjava.ast.ModelDeclPragma
-
- childAt(int) -
Method in class escjava.ast.ModelMethodDeclPragma
-
- childAt(int) -
Method in class escjava.ast.ModelProgamModifierPragma
-
- childAt(int) -
Method in class escjava.ast.ModelTypePragma
-
- childAt(int) -
Method in class escjava.ast.ModifiesGroupPragma
-
- childAt(int) -
Method in class escjava.ast.NamedExprDeclPragma
-
- childAt(int) -
Method in class escjava.ast.NaryExpr
-
- childAt(int) -
Method in class escjava.ast.NestedModifierPragma
-
- childAt(int) -
Method in class escjava.ast.NotModifiedExpr
-
- childAt(int) -
Method in class escjava.ast.NotSpecifiedExpr
-
- childAt(int) -
Method in class escjava.ast.NothingExpr
-
- childAt(int) -
Method in class escjava.ast.NowarnPragma
-
- childAt(int) -
Method in class escjava.ast.NumericalQuantifiedExpr
-
- childAt(int) -
Method in class escjava.ast.ParsedSpecs
-
- childAt(int) -
Method in class escjava.ast.QuantifiedExpr
-
- childAt(int) -
Method in class escjava.ast.ReachModifierPragma
-
- childAt(int) -
Method in class escjava.ast.RefinePragma
-
- childAt(int) -
Method in class escjava.ast.ResExpr
-
- childAt(int) -
Method in class escjava.ast.RestoreFromCmd
-
- childAt(int) -
Method in class escjava.ast.SeqCmd
-
- childAt(int) -
Method in class escjava.ast.SetCompExpr
-
- childAt(int) -
Method in class escjava.ast.SetStmtPragma
-
- childAt(int) -
Method in class escjava.ast.SimpleCmd
-
- childAt(int) -
Method in class escjava.ast.SimpleModifierPragma
-
- childAt(int) -
Method in class escjava.ast.SimpleStmtPragma
-
- childAt(int) -
Method in class escjava.ast.SkolemConstantPragma
-
- childAt(int) -
Method in class escjava.ast.Spec
-
- childAt(int) -
Method in class escjava.ast.StillDeferredDeclPragma
-
- childAt(int) -
Method in class escjava.ast.SubGetsCmd
-
- childAt(int) -
Method in class escjava.ast.SubSubGetsCmd
-
- childAt(int) -
Method in class escjava.ast.SubstExpr
-
- childAt(int) -
Method in class escjava.ast.TypeExpr
-
- childAt(int) -
Method in class escjava.ast.VarDeclModifierPragma
-
- childAt(int) -
Method in class escjava.ast.VarExprModifierPragma
-
- childAt(int) -
Method in class escjava.ast.VarInCmd
-
- childAt(int) -
Method in class escjava.ast.WildRefExpr
-
- childAt(int) -
Method in class javafe.ast.ASTNode
- Return the first-but-ith child of a node.
- childAt(int) -
Method in class javafe.ast.AmbiguousMethodInvocation
-
- childAt(int) -
Method in class javafe.ast.AmbiguousVariableAccess
-
- childAt(int) -
Method in class javafe.ast.ArrayInit
-
- childAt(int) -
Method in class javafe.ast.ArrayRefExpr
-
- childAt(int) -
Method in class javafe.ast.ArrayType
-
- childAt(int) -
Method in class javafe.ast.AssertStmt
-
- childAt(int) -
Method in class javafe.ast.BinaryExpr
-
- childAt(int) -
Method in class javafe.ast.BlockStmt
-
- childAt(int) -
Method in class javafe.ast.BreakStmt
-
- childAt(int) -
Method in class javafe.ast.CastExpr
-
- childAt(int) -
Method in class javafe.ast.CatchClause
-
- childAt(int) -
Method in class javafe.ast.ClassDecl
-
- childAt(int) -
Method in class javafe.ast.ClassDeclStmt
-
- childAt(int) -
Method in class javafe.ast.ClassLiteral
-
- childAt(int) -
Method in class javafe.ast.CompilationUnit
-
- childAt(int) -
Method in class javafe.ast.CompoundName
-
- childAt(int) -
Method in class javafe.ast.CondExpr
-
- childAt(int) -
Method in class javafe.ast.ConstructorDecl
-
- childAt(int) -
Method in class javafe.ast.ConstructorInvocation
-
- childAt(int) -
Method in class javafe.ast.ContinueStmt
-
- childAt(int) -
Method in class javafe.ast.DoStmt
-
- childAt(int) -
Method in class javafe.ast.ErrorType
-
- childAt(int) -
Method in class javafe.ast.EvalStmt
-
- childAt(int) -
Method in class javafe.ast.ExprObjectDesignator
-
- childAt(int) -
Method in class javafe.ast.FieldAccess
-
- childAt(int) -
Method in class javafe.ast.FieldDecl
-
- childAt(int) -
Method in class javafe.ast.ForStmt
-
- childAt(int) -
Method in class javafe.ast.FormalParaDecl
-
- childAt(int) -
Method in class javafe.ast.IdentifierNode
-
- childAt(int) -
Method in class javafe.ast.IfStmt
-
- childAt(int) -
Method in class javafe.ast.InitBlock
-
- childAt(int) -
Method in class javafe.ast.InstanceOfExpr
-
- childAt(int) -
Method in class javafe.ast.InterfaceDecl
-
- childAt(int) -
Method in class javafe.ast.JavafePrimitiveType
-
- childAt(int) -
Method in class javafe.ast.LabelStmt
-
- childAt(int) -
Method in class javafe.ast.LiteralExpr
-
- childAt(int) -
Method in class javafe.ast.LocalVarDecl
-
- childAt(int) -
Method in class javafe.ast.MethodDecl
-
- childAt(int) -
Method in class javafe.ast.MethodInvocation
-
- childAt(int) -
Method in class javafe.ast.NewArrayExpr
-
- childAt(int) -
Method in class javafe.ast.NewInstanceExpr
-
- childAt(int) -
Method in class javafe.ast.OnDemandImportDecl
-
- childAt(int) -
Method in class javafe.ast.ParenExpr
-
- childAt(int) -
Method in class javafe.ast.ReturnStmt
-
- childAt(int) -
Method in class javafe.ast.SimpleName
-
- childAt(int) -
Method in class javafe.ast.SingleTypeImportDecl
-
- childAt(int) -
Method in class javafe.ast.SkipStmt
-
- childAt(int) -
Method in class javafe.ast.SuperObjectDesignator
-
- childAt(int) -
Method in class javafe.ast.SwitchLabel
-
- childAt(int) -
Method in class javafe.ast.SwitchStmt
-
- childAt(int) -
Method in class javafe.ast.SynchronizeStmt
-
- childAt(int) -
Method in class javafe.ast.ThisExpr
-
- childAt(int) -
Method in class javafe.ast.ThrowStmt
-
- childAt(int) -
Method in class javafe.ast.TryCatchStmt
-
- childAt(int) -
Method in class javafe.ast.TryFinallyStmt
-
- childAt(int) -
Method in class javafe.ast.TypeName
-
- childAt(int) -
Method in class javafe.ast.TypeObjectDesignator
-
- childAt(int) -
Method in class javafe.ast.UnaryExpr
-
- childAt(int) -
Method in class javafe.ast.VarDeclStmt
-
- childAt(int) -
Method in class javafe.ast.VariableAccess
-
- childAt(int) -
Method in class javafe.ast.WhileStmt
-
- childAt(int) -
Method in class javafe.tc.TypeSig
-
- childCount() -
Method in class escjava.ast.AnOverview
- Return the number of children a node has.
- childCount() -
Method in class escjava.ast.ArrayRangeRefExpr
-
- childCount() -
Method in class escjava.ast.Call
-
- childCount() -
Method in class escjava.ast.CmdCmdCmd
-
- childCount() -
Method in class escjava.ast.CondExprModifierPragma
-
- childCount() -
Method in class escjava.ast.Condition
-
- childCount() -
Method in class escjava.ast.DecreasesInfo
-
- childCount() -
Method in class escjava.ast.DefPred
-
- childCount() -
Method in class escjava.ast.DefPredApplExpr
-
- childCount() -
Method in class escjava.ast.DefPredLetExpr
-
- childCount() -
Method in class escjava.ast.DependsPragma
-
- childCount() -
Method in class escjava.ast.DynInstCmd
-
- childCount() -
Method in class escjava.ast.EscPrimitiveType
-
- childCount() -
Method in class escjava.ast.EverythingExpr
-
- childCount() -
Method in class escjava.ast.ExprCmd
-
- childCount() -
Method in class escjava.ast.ExprDeclPragma
-
- childCount() -
Method in class escjava.ast.ExprModifierPragma
-
- childCount() -
Method in class escjava.ast.ExprStmtPragma
-
- childCount() -
Method in class escjava.ast.GCExpr
- Return the number of children a node has.
- childCount() -
Method in class escjava.ast.GeneralizedQuantifiedExpr
-
- childCount() -
Method in class escjava.ast.GetsCmd
-
- childCount() -
Method in class escjava.ast.GhostDeclPragma
-
- childCount() -
Method in class escjava.ast.GuardExpr
-
- childCount() -
Method in class escjava.ast.GuardedCmd
- Return the number of children a node has.
- childCount() -
Method in class escjava.ast.IdExprDeclPragma
-
- childCount() -
Method in class escjava.ast.IdentifierModifierPragma
-
- childCount() -
Method in class escjava.ast.ImportPragma
-
- childCount() -
Method in class escjava.ast.LabelExpr
-
- childCount() -
Method in class escjava.ast.LockSetExpr
-
- childCount() -
Method in class escjava.ast.LoopCmd
-
- childCount() -
Method in class escjava.ast.MapsExprModifierPragma
-
- childCount() -
Method in class escjava.ast.ModelConstructorDeclPragma
-
- childCount() -
Method in class escjava.ast.ModelDeclPragma
-
- childCount() -
Method in class escjava.ast.ModelMethodDeclPragma
-
- childCount() -
Method in class escjava.ast.ModelProgamModifierPragma
-
- childCount() -
Method in class escjava.ast.ModelTypePragma
-
- childCount() -
Method in class escjava.ast.ModifiesGroupPragma
-
- childCount() -
Method in class escjava.ast.NamedExprDeclPragma
-
- childCount() -
Method in class escjava.ast.NaryExpr
-
- childCount() -
Method in class escjava.ast.NestedModifierPragma
-
- childCount() -
Method in class escjava.ast.NotModifiedExpr
-
- childCount() -
Method in class escjava.ast.NotSpecifiedExpr
-
- childCount() -
Method in class escjava.ast.NothingExpr
-
- childCount() -
Method in class escjava.ast.NowarnPragma
-
- childCount() -
Method in class escjava.ast.NumericalQuantifiedExpr
-
- childCount() -
Method in class escjava.ast.ParsedSpecs
-
- childCount() -
Method in class escjava.ast.QuantifiedExpr
-
- childCount() -
Method in class escjava.ast.ReachModifierPragma
-
- childCount() -
Method in class escjava.ast.RefinePragma
-
- childCount() -
Method in class escjava.ast.ResExpr
-
- childCount() -
Method in class escjava.ast.RestoreFromCmd
-
- childCount() -
Method in class escjava.ast.SeqCmd
-
- childCount() -
Method in class escjava.ast.SetCompExpr
-
- childCount() -
Method in class escjava.ast.SetStmtPragma
-
- childCount() -
Method in class escjava.ast.SimpleCmd
-
- childCount() -
Method in class escjava.ast.SimpleModifierPragma
-
- childCount() -
Method in class escjava.ast.SimpleStmtPragma
-
- childCount() -
Method in class escjava.ast.SkolemConstantPragma
-
- childCount() -
Method in class escjava.ast.Spec
-
- childCount() -
Method in class escjava.ast.StillDeferredDeclPragma
-
- childCount() -
Method in class escjava.ast.SubGetsCmd
-
- childCount() -
Method in class escjava.ast.SubSubGetsCmd
-
- childCount() -
Method in class escjava.ast.SubstExpr
-
- childCount() -
Method in class escjava.ast.TypeExpr
-
- childCount() -
Method in class escjava.ast.VarDeclModifierPragma
-
- childCount() -
Method in class escjava.ast.VarExprModifierPragma
-
- childCount() -
Method in class escjava.ast.VarInCmd
-
- childCount() -
Method in class escjava.ast.WildRefExpr
-
- childCount() -
Method in class javafe.ast.ASTNode
- Return the number of children a node has.
- childCount() -
Method in class javafe.ast.AmbiguousMethodInvocation
-
- childCount() -
Method in class javafe.ast.AmbiguousVariableAccess
-
- childCount() -
Method in class javafe.ast.ArrayInit
-
- childCount() -
Method in class javafe.ast.ArrayRefExpr
-
- childCount() -
Method in class javafe.ast.ArrayType
-
- childCount() -
Method in class javafe.ast.AssertStmt
-
- childCount() -
Method in class javafe.ast.BinaryExpr
-
- childCount() -
Method in class javafe.ast.BlockStmt
-
- childCount() -
Method in class javafe.ast.BreakStmt
-
- childCount() -
Method in class javafe.ast.CastExpr
-
- childCount() -
Method in class javafe.ast.CatchClause
-
- childCount() -
Method in class javafe.ast.ClassDecl
-
- childCount() -
Method in class javafe.ast.ClassDeclStmt
-
- childCount() -
Method in class javafe.ast.ClassLiteral
-
- childCount() -
Method in class javafe.ast.CompilationUnit
-
- childCount() -
Method in class javafe.ast.CompoundName
-
- childCount() -
Method in class javafe.ast.CondExpr
-
- childCount() -
Method in class javafe.ast.ConstructorDecl
-
- childCount() -
Method in class javafe.ast.ConstructorInvocation
-
- childCount() -
Method in class javafe.ast.ContinueStmt
-
- childCount() -
Method in class javafe.ast.DoStmt
-
- childCount() -
Method in class javafe.ast.ErrorType
-
- childCount() -
Method in class javafe.ast.EvalStmt
-
- childCount() -
Method in class javafe.ast.ExprObjectDesignator
-
- childCount() -
Method in class javafe.ast.FieldAccess
-
- childCount() -
Method in class javafe.ast.FieldDecl
-
- childCount() -
Method in class javafe.ast.ForStmt
-
- childCount() -
Method in class javafe.ast.FormalParaDecl
-
- childCount() -
Method in class javafe.ast.IdentifierNode
-
- childCount() -
Method in class javafe.ast.IfStmt
-
- childCount() -
Method in class javafe.ast.InitBlock
-
- childCount() -
Method in class javafe.ast.InstanceOfExpr
-
- childCount() -
Method in class javafe.ast.InterfaceDecl
-
- childCount() -
Method in class javafe.ast.JavafePrimitiveType
-
- childCount() -
Method in class javafe.ast.LabelStmt
-
- childCount() -
Method in class javafe.ast.LiteralExpr
-
- childCount() -
Method in class javafe.ast.LocalVarDecl
-
- childCount() -
Method in class javafe.ast.MethodDecl
-
- childCount() -
Method in class javafe.ast.MethodInvocation
-
- childCount() -
Method in class javafe.ast.NewArrayExpr
-
- childCount() -
Method in class javafe.ast.NewInstanceExpr
-
- childCount() -
Method in class javafe.ast.OnDemandImportDecl
-
- childCount() -
Method in class javafe.ast.ParenExpr
-
- childCount() -
Method in class javafe.ast.ReturnStmt
-
- childCount() -
Method in class javafe.ast.SimpleName
-
- childCount() -
Method in class javafe.ast.SingleTypeImportDecl
-
- childCount() -
Method in class javafe.ast.SkipStmt
-
- childCount() -
Method in class javafe.ast.SuperObjectDesignator
-
- childCount() -
Method in class javafe.ast.SwitchLabel
-
- childCount() -
Method in class javafe.ast.SwitchStmt
-
- childCount() -
Method in class javafe.ast.SynchronizeStmt
-
- childCount() -
Method in class javafe.ast.ThisExpr
-
- childCount() -
Method in class javafe.ast.ThrowStmt
-
- childCount() -
Method in class javafe.ast.TryCatchStmt
-
- childCount() -
Method in class javafe.ast.TryFinallyStmt
-
- childCount() -
Method in class javafe.ast.TypeName
-
- childCount() -
Method in class javafe.ast.TypeObjectDesignator
-
- childCount() -
Method in class javafe.ast.UnaryExpr
-
- childCount() -
Method in class javafe.ast.VarDeclStmt
-
- childCount() -
Method in class javafe.ast.VariableAccess
-
- childCount() -
Method in class javafe.ast.WhileStmt
-
- childCount() -
Method in class javafe.tc.TypeSig
- *
ASTNode functions: *
*
- childError -
Static variable in class escjava.ColorOptions
-
- children() -
Method in class javafe.filespace.HashTree
- An enumeration of this node's direct children.
- children() -
Method in class javafe.filespace.LeafTree
- *
Fetching and counting children: *
*
- children() -
Method in class javafe.filespace.PreloadedTree
- *
Fetching and counting children: *
*
- children() -
Method in class javafe.filespace.Tree
- An enumeration of this node's direct children.
- children -
Variable in class javafe.parser.PunctuationPrefixTree
-
- chkStatus -
Static variable in class escjava.translate.NoWarn
- *
Global nowarns: *
*
- chkToMsg(int, boolean) -
Static method in class escjava.translate.ErrorMsg
-
- choosecmd(GuardedCmd, GuardedCmd) -
Static method in class escjava.translate.GC
-
- classIdentifier -
Variable in class javafe.reader.ASTClassFileParser
- The identifier of the class being parsed.
- classLocation -
Variable in class javafe.reader.ASTClassFileParser
- A dummy location representing the class being parsed.
- classLocation -
Static variable in class javafe.reader.DescriptorParser
- A dummy location representing the class being parsed.
- classMembers -
Variable in class javafe.reader.ASTClassFileParser
- The class members of the class being parsed.
- classPackage -
Variable in class javafe.reader.ASTClassFileParser
- The package name of the class being parsed.
- classPrefix -
Variable in class javafe.ast.ThisExpr
-
- classpathText -
Variable in class escjava.gui.EscFrame
-
- clauseLoc -
Variable in class escjava.ast.ModifiesGroupPragma
-
- clauses -
Variable in class escjava.pa.generic.BinaryDecisionTreeAbstractor
-
- clauses -
Variable in class escjava.pa.generic.EnumClausesAbstractor
-
- clauses -
Variable in class escjava.pa.generic.EnumMaxClausesFindMinAbstractor
-
- clauses -
Variable in class escjava.pa.generic.EnumNFindK
-
- clean() -
Method in class escjava.translate.AuxInfoLink
-
- cleancopy(TypeDeclVec) -
Method in class escjava.RefinementSequence
-
- cleancopy(TypeDecl) -
Method in class escjava.RefinementSequence
-
- cleancopy(TypeDeclElem) -
Method in class escjava.RefinementSequence
-
- cleancopy(FormalParaDeclVec, boolean) -
Method in class escjava.RefinementSequence
-
- clear(boolean) -
Method in class escjava.Main
-
- clear() -
Method in class escjava.gui.TaskQueue
-
- clear(boolean) -
Method in class javafe.FrontEndTool
- Called to clear any static initializations, so that the parser
can be called multiple times within one process.
- clear(ArrayList) -
Static method in class javafe.InputEntry
-
- clear() -
Method in class javafe.InputEntry
-
- clear() -
Method in class javafe.parser.Token
- Clear the current token.
- clear() -
Method in class javafe.parser.TokenQueue
- Empties lookahead queue.
- clear() -
Method in class javafe.reader.StandardTypeReader
-
- clear() -
Static method in class javafe.tc.OutsideEnv
-
- clear() -
Static method in class javafe.tc.TypeSig
-
- clear() -
Static method in class javafe.util.ErrorSet
- Resets all error and warning counts.
- clear() -
Static method in class javafe.util.LocationManagerCorrelatedReader
-
- clear() -
Method in class javafe.util.Set
- Remove all our elements
- clear() -
Method in class javafe.util.StackVector
- Reset us to the state where we contain only 1 Vector, which has
zero-length.
- clearCheck() -
Method in class escjava.gui.GUI.EscTreeValue
-
- clearCheck() -
Method in class escjava.gui.GUI.RDTreeValue
-
- clearCheck() -
Method in class escjava.gui.GUI.TDTreeValue
-
- clearMark() -
Method in class javafe.util.BufferedCorrelatedReader
- Removes the mark (if any) from the input stream.
- clearMark() -
Method in class javafe.util.CorrelatedReader
- Removes the mark (if any) from the input stream.
- clearMark() -
Method in class javafe.util.FilterCorrelatedReader
- See documentation in superclass.
- clone(boolean) -
Method in class javafe.ast.ASTNode
-
- clone() -
Method in class javafe.ast.ASTNode
- Clone node, where the clone has the same decorations as original.
- clone() -
Method in class javafe.util.Set
-
- cloneGuardedCommand(GuardedCmd) -
Method in class escjava.translate.Translate
- This method returns a guarded command
G that is like
gc except that where gc contains a mutable command,
G contains a fresh copy of that command.
- close() -
Method in class escjava.parser.ErrorPragmaParser
- No work to close us.
- close() -
Method in class escjava.parser.EscPragmaParser
- Closes this pragma parser including its scanner and pending Javadoc comment.
- close() -
Method in class escjava.prover.Simplify
- Close us.
- close() -
Method in class escjava.prover.SubProcess
- Close this subprocess.
- close() -
Method in class escjava.prover.TeeOutputStream
- Closes this output stream and releases any system resources
associated with the stream.
- close() -
Method in class javafe.parser.Lex
- Closes the
CorrelatedReader underlying
this, clears the set of collected lexical pragmas,
and in other ways frees up resources associated with
this.
- close() -
Method in interface javafe.parser.PragmaParser
- Stop parsing the current reader.
- close() -
Method in class javafe.util.BufferedCorrelatedReader
- Closes us.
- close() -
Method in class javafe.util.CorrelatedReader
- Closes us.
- close() -
Method in class javafe.util.FileCorrelatedReader
- Closes us.
- close() -
Method in class javafe.util.FilterCorrelatedReader
- Closes us.
- close() -
Method in class javafe.util.LocationManagerCorrelatedReader
- Closes us.
- closeForClause() -
Static method in class escjava.translate.TrAnExpr
-
- cmd -
Variable in class escjava.ast.CmdCmdCmd
-
- cmd -
Variable in class escjava.ast.ExprCmd
-
- cmd -
Variable in class escjava.ast.SimpleCmd
-
- cmds -
Variable in class escjava.ast.SeqCmd
-
- code -
Variable in class escjava.pa.PredicateAbstraction
-
- code -
Variable in class escjava.translate.DefGCmd
code is the StackVector instance and is used to hold the
definednes guarded commands for each method.
- code -
Variable in class escjava.translate.Translate
- Contains the guarded commands generated so far for the current method.
- code -
Variable in class javafe.parser.PunctuationPrefixTree
-
- codevec -
Variable in class escjava.translate.Translate
-
- collectAxioms(FindContributors) -
Static method in class escjava.translate.GetSpec
- Collects the axioms in
scope.
- collectFields(Expr, Set) -
Static method in class escjava.translate.GetSpec
-
- collectInvariants(FindContributors, Hashtable) -
Static method in class escjava.translate.GetSpec
-
- collectInvariantsAxsToAdd -
Static variable in class escjava.translate.GetSpec
- Collects the invariants in
scope.
- collectParamsAndGlobals(Spec, FindContributors) -
Static method in class escjava.translate.GetSpec
- Collects the parameters of
spec.args and the static fields
in scope, whose types are class types.
- colors -
Static variable in class escjava.vcGeneration.TDisplay
-
- combineFields(FieldDecl, FieldDecl) -
Method in class escjava.RefinementSequence
-
- combineModifies(ModifierPragmaVec) -
Method in class escjava.AnnotationHandler
-
- combineNames(String, String, String) -
Static method in class javafe.filespace.Resolve
- Combine two names using a separator if both are non-empty.
- combineRoutine(RoutineDecl, RoutineDecl) -
Method in class escjava.RefinementSequence
-
- combineType(TypeDecl, TypeDecl, boolean) -
Method in class escjava.RefinementSequence
-
- combineUniverses(ASTNode, ASTNode) -
Method in class escjava.RefinementSequence
-
- combinedString() -
Method in class escjava.gui.GUI.EscTreeValue
-
- combinedString() -
Method in class escjava.gui.GUI.RDTreeValue
-
- commentMark -
Variable in class escjava.vcGeneration.PrettyPrinter
-
- comp(int, int, String) -
Static method in class escjava.ast.TagConstants
-
- compareStringToFile(String, String) -
Static method in class junitutils.Utils
- Compares the given string to the content of the given file using
a comparator that ignores platform differences in line-endings.
- compile(String[]) -
Static method in class escjava.Main
- An entry point for the tool useful for executing tests,
since it returns the exit code.
- completed -
Variable in class escjava.translate.Translate.EverythingLoc
-
- components(Tree, String) -
Static method in class javafe.filespace.PkgTree
- Enumerate all the components of package P with extension E in
sorted order (of labels).
- compositeClassPath -
Variable in class javafe.FrontEndTool
-
- compositeSourcePath -
Variable in class javafe.FrontEndTool
- Setup: initialize the front end using the standard
front-end-tool option variables (
Options.userPath,
Options.sysPath).
- computationDone -
Variable in class escjava.vcGeneration.VcGenerator
-
- compute(GuardedCmd, InitialState, Translate) -
Static method in class escjava.pa.Traverse
-
- compute(GuardedCmd) -
Static method in class escjava.sp.SPVC
-
- compute(GuardedCmd) -
Static method in class escjava.translate.ATarget
-
- compute(GuardedCmd, Expr, Expr) -
Static method in class escjava.translate.Ejp
-
- compute(GuardedCmd, Expr, Expr, String, VarMap) -
Static method in class escjava.translate.Ejp
-
- compute(Expr, PrintStream) -
Static method in class escjava.translate.VcToString
- Prints
e as a verification-condition string to
to.
- computeBody(RoutineDecl, InitialState) -
Method in class escjava.Main
- This method computes the guarded command (including assuming
the precondition, the translated body, the checked
postcondition, and the modifies constraints) for the method or
constructor
r in scope scope.
- computeFreshUsage() -
Method in class escjava.ast.DerivedMethodDecl
-
- computeHelper(GuardedCmd, GuardedCmd, Set) -
Static method in class escjava.pa.Traverse
-
- computeInlineSettings(RoutineDecl, ExprVec, InlineSettings, int) -
Method in class escjava.translate.Translate
- Computes the inlining settings for a given call.
- computeLastVarUses(GuardedCmd, RefInt, Hashtable) -
Static method in class escjava.sp.DSA
-
- computeMentionsSet(ASTNode, Set) -
Static method in class escjava.translate.ATarget
-
- computeN(GuardedCmd) -
Static method in class escjava.sp.SPVC
-
- computeNotWrong(GuardedCmd) -
Method in class escjava.sp.SPVC
-
- computePC(Expr, PrintStream) -
Static method in class escjava.translate.VcToString
-
- computeTypeSpecific(Expr, PrintStream) -
Static method in class escjava.translate.VcToString
- Prints
e as a simple-expression string to to.
- concretize(Vector) -
Method in class escjava.pa.GCProver
-
- concretize(jbdd) -
Method in class escjava.pa.GCProver
-
- cond -
Variable in class escjava.ast.CondExprModifierPragma
-
- condition(int, Expr, int) -
Static method in class escjava.translate.GC
-
- consistencyCheck -
Variable in class escjava.Options
-
- consolidateRefinements(ArrayList, CompilationUnit) -
Method in class escjava.RefinementSequence
-
- constantValueFitsIn(Object, PrimitiveType) -
Static method in class javafe.tc.ConstantExpr
-
- constants -
Variable in class javafe.reader.ASTClassFileParser
- The constant pool of the class being parsed.
- constructorSeq -
Variable in class javafe.tc.PrepTypeDeclaration
-
- contains(CondExprModifierPragma) -
Method in class escjava.ast.CondExprModifierPragmaVec
-
- contains(Condition) -
Method in class escjava.ast.ConditionVec
-
- contains(DecreasesInfo) -
Method in class escjava.ast.DecreasesInfoVec
-
- contains(DefPred) -
Method in class escjava.ast.DefPredVec
-
- contains(ExprDeclPragma) -
Method in class escjava.ast.ExprDeclPragmaVec
-
- contains(ExprModifierPragma) -
Method in class escjava.ast.ExprModifierPragmaVec
-
- contains(ExprStmtPragma) -
Method in class escjava.ast.ExprStmtPragmaVec
-
- contains(GenericVarDecl) -
Method in class escjava.ast.GenericVarDeclVec
-
- contains(GuardedCmd) -
Method in class escjava.ast.GuardedCmdVec
-
- contains(LocalVarDecl) -
Method in class escjava.ast.LocalVarDeclVec
-
- contains(ModifiesGroupPragma) -
Method in class escjava.ast.ModifiesGroupPragmaVec
-
- contains(VarExprModifierPragma) -
Method in class escjava.ast.VarExprModifierPragmaVec
-
- contains(CatchClause) -
Method in class javafe.ast.CatchClauseVec
-
- contains(Expr) -
Method in class javafe.ast.ExprVec
-
- contains(FieldDecl) -
Method in class javafe.ast.FieldDeclVec
-
- contains(FormalParaDecl) -
Method in class javafe.ast.FormalParaDeclVec
-
- contains(Identifier) -
Method in class javafe.ast.IdentifierVec
-
- contains(ImportDecl) -
Method in class javafe.ast.ImportDeclVec
-
- contains(LexicalPragma) -
Method in class javafe.ast.LexicalPragmaVec
-
- contains(MethodDecl) -
Method in class javafe.ast.MethodDeclVec
-
- contains(ModifierPragma) -
Method in class javafe.ast.ModifierPragmaVec
-
- contains(Stmt) -
Method in class javafe.ast.StmtVec
-
- contains(TypeDeclElem) -
Method in class javafe.ast.TypeDeclElemVec
-
- contains(TypeDecl) -
Method in class javafe.ast.TypeDeclVec
-
- contains(TypeModifierPragma) -
Method in class javafe.ast.TypeModifierPragmaVec
-
- contains(TypeName) -
Method in class javafe.ast.TypeNameVec
-
- contains(VarInit) -
Method in class javafe.ast.VarInitVec
-
- contains(TypeSig) -
Method in class javafe.tc.TypeSigVec
-
- contains(Object) -
Method in class javafe.util.Set
- Do we contain a particular element?
- contains(Object) -
Method in class javafe.util.StackVector
- Return true iff the top Vector contains o.
- containsAny(Set) -
Method in class javafe.util.Set
- Returns whether or not the set has any element in common with
s.
- containsEndOfConstruct(String, int) -
Method in class escjava.translate.AssocDeclClipPolicy
-
- containsEndOfConstruct(String, int) -
Method in class javafe.util.ClipPolicy
-
- containsSpecOnly(CompilationUnit) -
Method in class escjava.reader.EscTypeReader
- Does a CompilationUnit contain a specOnly TypeDecl?
- contents -
Variable in class javafe.InputEntry
-
- context -
Variable in class escjava.prover.SimplifyResult
-
- continueLabel(Stmt) -
Method in class escjava.translate.Translate
-
- continuePragma(Token) -
Method in class escjava.parser.EscPragmaParser
-
- contributorFields -
Variable in class escjava.backpred.FindContributors
- The set of fields (elementType FieldDecl) we've determined to be
contributors so far.
- contributorInvariants -
Variable in class escjava.backpred.FindContributors
- The set of invariants (elementType ExprDeclPragmas) we've
determined to be contributors so far.
- contributorTypes -
Variable in class escjava.backpred.FindContributors
- The set of TypeSigs we've determined to be contributors so far.
- copy() -
Method in class escjava.ast.CondExprModifierPragmaVec
-
- copy() -
Method in class escjava.ast.ConditionVec
-
- copy() -
Method in class escjava.ast.DecreasesInfoVec
-
- copy() -
Method in class escjava.ast.DefPredVec
-
- copy() -
Method in class escjava.ast.ExprDeclPragmaVec
-
- copy() -
Method in class escjava.ast.ExprModifierPragmaVec
-
- copy() -
Method in class escjava.ast.ExprStmtPragmaVec
-
- copy() -
Method in class escjava.ast.GenericVarDeclVec
-
- copy() -
Method in class escjava.ast.GuardedCmdVec
-
- copy() -
Method in class escjava.ast.LocalVarDeclVec
-
- copy() -
Method in class escjava.ast.ModifiesGroupPragmaVec
-
- copy() -
Method in class escjava.ast.VarExprModifierPragmaVec
-
- copy() -
Method in class javafe.ast.CatchClauseVec
-
- copy() -
Method in class javafe.ast.ExprVec
-
- copy() -
Method in class javafe.ast.FieldDeclVec
-
- copy() -
Method in class javafe.ast.FormalParaDeclVec
-
- copy() -
Method in class javafe.ast.IdentifierVec
-
- copy() -
Method in class javafe.ast.ImportDeclVec
-
- copy() -
Method in class javafe.ast.LexicalPragmaVec
-
- copy() -
Method in class javafe.ast.MethodDeclVec
-
- copy() -
Method in class javafe.ast.ModifierPragmaVec
-
- copy() -
Method in class javafe.ast.StmtVec
-
- copy() -
Method in class javafe.ast.TypeDeclElemVec
-
- copy() -
Method in class javafe.ast.TypeDeclVec
-
- copy() -
Method in class javafe.ast.TypeModifierPragmaVec
-
- copy() -
Method in class javafe.ast.TypeNameVec
-
- copy() -
Method in class javafe.ast.VarInitVec
-
- copy() -
Method in class javafe.tc.TypeSigVec
-
- copyInto(Token) -
Method in class javafe.parser.Token
- Copy all the fields of
this into
dst.
- copyInto(Object[]) -
Method in class javafe.util.StackVector
-
- copyName(Name, RoutineDecl) -
Static method in class escjava.translate.InlineConstructor
-
- copyType(VarInit, VarInit) -
Static method in class escjava.tc.FlowInsensitiveChecks
- Copy the Type associated with an expression by the typechecking pass to
another Expr.
- copyType(Type, RoutineDecl) -
Static method in class escjava.translate.InlineConstructor
-
- copyTypeName(TypeName, RoutineDecl) -
Static method in class escjava.translate.InlineConstructor
-
- copyUniverses(ASTNode, ASTNode) -
Static method in class javafe.tc.FlowInsensitiveChecks
-
- coqRename(TypeInfo) -
Method in class escjava.vcGeneration.coq.CoqProver
- Rename the type, ie. the name
TypeInfo.old to
a proper Coq name in the variable TypeInfo.def
- coqRename(VariableInfo) -
Method in class escjava.vcGeneration.coq.CoqProver
- Rename the variable, ie. the name
VariableInfo.old to
a proper Coq name in the variable VariableInfo.def.
- count -
Variable in class escjava.ast.CondExprModifierPragmaVec
-
- count -
Variable in class escjava.ast.ConditionVec
-
- count -
Variable in class escjava.ast.DecreasesInfoVec
-
- count -
Variable in class escjava.ast.DefPredVec
-
- count -
Variable in class escjava.ast.ExprDeclPragmaVec
-
- count -
Variable in class escjava.ast.ExprModifierPragmaVec
-
- count -
Variable in class escjava.ast.ExprStmtPragmaVec
-
- count -
Variable in class escjava.ast.GenericVarDeclVec
-
- count -
Variable in class escjava.ast.GuardedCmdVec
-
- count -
Variable in class escjava.ast.LocalVarDeclVec
-
- count -
Variable in class escjava.ast.ModifiesGroupPragmaVec
-
- count -
Variable in class escjava.ast.VarExprModifierPragmaVec
-
- count(FieldDecl) -
Method in class escjava.translate.Frame.ModifiesIterator
- Returns the number of times the argument is in the 'done'
list
- count -
Static variable in class escjava.translate.Translate.Strings
-
- count(ASTNode) -
Static method in class javafe.CountLines
-
- count -
Variable in class javafe.ast.CatchClauseVec
-
- count -
Variable in class javafe.ast.ExprVec
-
- count -
Variable in class javafe.ast.FieldDeclVec
-
- count -
Variable in class javafe.ast.FormalParaDeclVec
-
- count -
Variable in class javafe.ast.IdentifierVec
-
- count -
Variable in class javafe.ast.ImportDeclVec
-
- count -
Variable in class javafe.ast.LexicalPragmaVec
-
- count -
Variable in class javafe.ast.MethodDeclVec
-
- count -
Variable in class javafe.ast.ModifierPragmaVec
-
- count -
Variable in class javafe.ast.StmtVec
-
- count -
Variable in class javafe.ast.TypeDeclElemVec
-
- count -
Variable in class javafe.ast.TypeDeclVec
-
- count -
Variable in class javafe.ast.TypeModifierPragmaVec
-
- count -
Variable in class javafe.ast.TypeNameVec
-
- count -
Variable in class javafe.ast.VarInitVec
-
- count -
Variable in class javafe.tc.TypeSigVec
-
- countChar(String, char) -
Static method in class javafe.filespace.StringUtil
- Count the number of times a given character occurs in a String:
- countDuplicates() -
Method in class javafe.filespace.UnionTree
- Return the number of nodes corresponding to this one there are
in the underlying Trees.
- countFreeVarsAccesses -
Variable in class escjava.tc.FlowInsensitiveChecks
- Counts the number of accesses of free variables and fields used for checking
the appropriateness of invariants.
- countParameters() -
Method in class javafe.reader.MethodSignature
- Count the number of parameter types in this method signature.
- counter -
Static variable in class escjava.vcGeneration.TNode
-
- counterexample -
Variable in class escjava.Options
-
- createFakeLoc(String) -
Static method in class javafe.util.Location
- Create a fake location described by description.
- createForall(Expr, Expr, ArrayList) -
Static method in class escjava.translate.TrAnExpr
-
- createFunctionCall(RoutineDecl, ArrayList, Hashtable) -
Static method in class escjava.translate.TrAnExpr
-
- createMethodDecl(MethodDecl, TypeDecl, ConstructorDecl, Identifier, int) -
Static method in class escjava.translate.InlineConstructor
-
- createReaderFromMark(int) -
Method in class javafe.util.BufferedCorrelatedReader
- Creates a
CorrelatedReader object for the input
text from the marked position, to the current position.
- createReaderFromMark(int) -
Method in class javafe.util.CorrelatedReader
- Creates a
CorrelatedReader object for the input
text from the marked position, to the current position.
- createReaderFromMark(int) -
Method in class javafe.util.FilterCorrelatedReader
-
- createTDNode(TypeDecl, DefaultMutableTreeNode) -
Method in class escjava.gui.GUI
-
- createVarVariant(GenericVarDecl, String) -
Static method in class escjava.translate.GetSpec
- * Given a GenericVarDecl named "x@old", returns a VariableAccess to a *
fresh LocalVarDecl named "x@
". * * This handles ESCJ 23b case 13.
- createWholeFileLoc(GenericFile) -
Static method in class javafe.util.FileCorrelatedReader
- Create a whole file location for a given GenericFile.
- createWholeFileLoc(GenericFile) -
Static method in class javafe.util.Location
- Create a whole file location corresponding to the given GenericFile.
- cu -
Variable in class escjava.gui.GUI.GFCUTreeValue
-
- curLineNo -
Variable in class javafe.util.LocationManagerCorrelatedReader
- The current line number; that is, the number of
we've read from our stream so far + 1.
- curNdx -
Variable in class javafe.util.BufferedCorrelatedReader
- The index of the next character to be read from the buffer.
- current() -
Static method in class javafe.filespace.ClassPath
- Return our current classpath; if the Java system property
java.class.path.skip is set to n, we
ignore the first n components of the path.
- currentAlloc -
Static variable in class escjava.translate.TrAnExpr
-
- currentOutputFrame -
Variable in class escjava.gui.GUI
-
- currentParent -
Variable in class escjava.vcGeneration.VcGenerator
- This attribute is used by the next function to save the current parent of the node
we may create.
- currentProject -
Static variable in class escjava.gui.Project
-
- currentStackBottom -
Variable in class javafe.util.StackVector
-
- currentState -
Static variable in class escjava.translate.TrAnExpr
-
- currentTime() -
Static method in class javafe.Tool
-
- currentdir -
Variable in class javafe.Options
- Option holding the current working directory.
- currentdirText -
Variable in class escjava.gui.EscFrame
-
- cvc3 -
Static variable in class escjava.ProverManager
-
DefGCmd implements the definedness guarded commands
for the requires clauses. DefGCmd instance.
debug is a central and convinient way of turning on/off
debug messages.
expr and its subexpressions with purity
information.
loop according to the fast option.
loop according to the safe option.
gc, that is, that are modified in some assignment
statement, not call statement, in gc.
SExp verbosely, using all its accessor
methods.
Env to System.out.
displayColumn.
preOrderCount and lastVarUse
are used to perform a dead-variable analysis on variables, so that
merges of variables can be smaller.
PragmaParser that reports an
client-chosen error message each time an annotation comment is
encountered. ErrorSet class is responsible for displaying
cautions, warnings, ordinary errors, and fatal errors to the user.
Lex.scanJavaExtensions(int) to
support "informal predicates". EscTypeReader is a StandardTypeReader
extended to understand ".spec" files.ESCTypeReader from a query engine, a
source reader, and a binary reader.
nth element in token queue.
other is a Name that
is component-wise equal to this.
other is a Name that
is component-wise equal to this.
String.valueOf(chars, 0,
chars.length); may be null.
Enumeration to compute all of its elements
P.T
exists.
expr is
defined.
FatalError is an unchecked exception thrown only by
ErrorSet.fatal that indicates that a fatal error has
been encountered, forcing all further processing to be
abandoned. FatalError exception.
FileCorrelatedReader is a
CorrelatedReader that reads its characters from a
stream that corresponds to a file.
child as the
underlying CorrelatedReader.
FrontEndTool is an abstract class for tools that use
our Java front end.
Integer), an atom (specified via a
String), or an existing S-expression (this case
leaves the argument unchanged).
TypeDecl associated with this,
including inherited ones.
vdecl
that has the tag tag, if any.
PushbackInputStream from the actual subprocess, or
null if we are closed.
SInt representing a given
int.
Atom representing a given symbol.
SrcTool.
EnvForTypeSig so that it "sees" ghost and model
fields if FlowInsensitiveChecks.inAnnotation is
true.gag is true, then no output is produced by
ErrorSet methods (useful for test harnesses).
id, as returned
by put since the last call to reset
It is assumed that id has indeed been returned by
put since the last call to reset.
ASTNode, or null
if the ASTNode has no decoration.
- get(GenericFile) -
Method in class javafe.reader.CachedReader
- Lookup a non-null GenericFile in the cache.
- get(String[], String) -
Static method in class javafe.tc.TypeSig
- If a TypeSig representing the package-member type named P.T
has been created, return it; otherwise, create such a TypeSig
then return it.
- getAccessibility(int) -
Method in class escjava.tc.FlowInsensitiveChecks
-
- getAllImplementsSet(MethodDecl) -
Method in class javafe.tc.TypeCheck
- Retrieves the set of interface
MethodDecls that a given
class MethodDecl implements.
- getAllOverrides(MethodDecl) -
Static method in class escjava.tc.FlowInsensitiveChecks
-
- getAllOverrides(MethodDecl) -
Method in class javafe.tc.TypeCheck
- Retrieves the set of
MethodDecls that a given
MethodDecl overrides or hides.
- getAllSpecs(RoutineDecl) -
Static method in class escjava.ast.Utils
-
- getArgType() -
Method in class escjava.vcGeneration.TMethodCall
- Returns a vector containing the types from the different arguments of
the MethodCall.
- getAtom() -
Method in class escjava.prover.Atom
- If we represent an atom, return it as an
Atom; otherwise,
throw SExpTypeError.
- getAtom() -
Method in class escjava.prover.SExp
- If we represent an atom, return it as an
Atom;
otherwise, throw SExpTypeError.
- getBasename(String) -
Static method in class javafe.filespace.Extension
- Return the basename of a filename -- the part of a filename
that preceeds its extension (if any).
- getBeforeMarkLocation() -
Method in class javafe.util.BufferedCorrelatedReader
- Returns the location of the character before the mark.
- getBooleanConstant(Object) -
Static method in class javafe.tc.ConstantExpr
-
- getBranchLabel(BranchStmt) -
Static method in class javafe.tc.FlowInsensitiveChecks
- Retrieves the
Stmt target of a BranchStmt.
- getBranchLabel(BranchStmt) -
Method in class javafe.tc.TypeCheck
- Retrieves the
Stmt target of a BranchStmt.
- getBufferFromMark(int) -
Method in class javafe.util.BufferedCorrelatedReader
- Returns a new buffer containing the contents of this BufferedCorrelatedReader's
buffer, from the marked position to the current position less
discard bytes (not characters).
- getCalledSpecs(RoutineDecl, ObjectDesignator, ExprVec, Expr, Hashtable, Hashtable) -
Static method in class escjava.translate.TrAnExpr
-
- getCanonicalID() -
Method in interface javafe.genericfile.GenericFile
- Return a String that canonically represents the identity of our
underlying file.
- getCanonicalID() -
Method in class javafe.genericfile.NormalGenericFile
-
- getCanonicalID() -
Method in class javafe.genericfile.UnopenableFile
-
- getCanonicalID() -
Method in class javafe.genericfile.ZipGenericFile
- Return a String that canonically represents the identity of our
underlying file.
- getChar() -
Method in class escjava.prover.SubProcess
-
- getChild(String) -
Method in class javafe.filespace.HashTree
- Fetch our direct child along the edge labelled label.
- getChild(String) -
Method in class javafe.filespace.PreloadedTree
-
- getChild(String) -
Method in class javafe.filespace.Tree
- Fetch our direct child along the edge labelled label.
- getChildAt(int) -
Method in class escjava.vcGeneration.TFunction
-
- getChildrenCount() -
Method in class javafe.filespace.LeafTree
-
- getChildrenCount() -
Method in class javafe.filespace.Tree
- Return a count of how many direct children we have:
- getChkStatus(int) -
Static method in class escjava.translate.NoWarn
-
- getChkStatus(int, int, int) -
Static method in class escjava.translate.NoWarn
- Returns how the check tag should be interpreted.
- getClassObject(TypeDecl) -
Method in class escjava.translate.Translate
-
- getClauses() -
Method in interface escjava.pa.generic.Abstractor
-
- getClauses() -
Method in class escjava.pa.generic.BinaryDecisionTreeAbstractor
-
- getClauses() -
Method in class escjava.pa.generic.EnumClausesAbstractor
-
- getClauses() -
Method in class escjava.pa.generic.EnumMaxClausesFindMinAbstractor
-
- getClauses() -
Method in class escjava.pa.generic.EnumNFindK
-
- getCode(int) -
Static method in class javafe.parser.TagConstants
-
- getCombinedBinaries(Name, String[], ArrayList) -
Method in class escjava.reader.RefinementCachedReader
-
- getCombinedMethodDecl(RoutineDecl) -
Static method in class escjava.translate.GetSpec
- * Implement GetCombinedMethodDecl from ESCJ 16c section 7:
* * Precondition: the type declaring rd has been typechecked.
- getCommonSpec(RoutineDecl, FindContributors, Hashtable) -
Static method in class escjava.translate.GetSpec
-
- getCompilationUnit() -
Method in class javafe.tc.TypeSig
- Get the non-null CompilationUnit we are associated with.
- getContainingClass() -
Method in class escjava.ast.DerivedMethodDecl
-
- getContext() -
Method in class escjava.prover.SimplifyResult
-
- getCorrStreamAt(int) -
Static method in class javafe.util.LocationManagerCorrelatedReader
- Return the LocationManagerCorrelatedReader associated with
streamId i.
- getDecorations() -
Method in class javafe.ast.ASTNode
-
- getDefpreds(Expr) -
Method in class escjava.translate.VcToString
-
- getDefpredsHelper(Expr) -
Method in class escjava.translate.VcToString
-
- getDirectOverrides(MethodDecl) -
Static method in class escjava.tc.FlowInsensitiveChecks
-
- getDoubleConstant(Object) -
Static method in class javafe.tc.ConstantExpr
-
- getElementUniverse(ASTNode) -
Static method in class javafe.parser.ParseUtil
-
- getEnclosingClass() -
Method in class escjava.tc.EnvForGhostLocals
- Return the intermost class enclosing the code that is checked
in this environment.
- getEnclosingClass() -
Method in class javafe.tc.Env
- Return the innermost class enclosing the code that is checked
in this environment.
- getEnclosingClass() -
Method in class javafe.tc.EnvForCU
- Return the intermost class enclosing the code that is checked
in this environment.
- getEnclosingClass() -
Method in class javafe.tc.EnvForEnclosedScope
- Return the intermost class enclosing the code that is checked
in this environment.
- getEnclosingClass() -
Method in class javafe.tc.EnvForLocalType
- Return the intermost class enclosing the code that is checked
in this environment.
- getEnclosingClass() -
Method in class javafe.tc.EnvForLocals
- Return the intermost class enclosing the code that is checked
in this environment.
- getEnclosingClass() -
Method in class javafe.tc.EnvForTypeSig
- Return the intermost class enclosing the code that is checked
in this environment.
- getEnclosingEnv() -
Method in class javafe.tc.TypeSig
- Return our enclosing environment.
- getEnclosingInstance() -
Method in class escjava.tc.EnvForGhostLocals
- If there is an enclosing instance in scope, then return the
(exact) type of the innermost such instance.
- getEnclosingInstance() -
Method in class javafe.tc.Env
- If there is an enclosing instance in scope, then return the
(exact) type of the innermost such instance.
- getEnclosingInstance() -
Method in class javafe.tc.EnvForCU
- If there is an enclosing instance in scope, then return the
(exact) type of the innermost such instance.
- getEnclosingInstance() -
Method in class javafe.tc.EnvForEnclosedScope
- If there is an enclosing instance in scope, then return the
(exact) type of the innermost such instance.
- getEnclosingInstance() -
Method in class javafe.tc.EnvForLocalType
- If there is an enclosing instance in scope, then return the
(exact) type of the innermost such instance.
- getEnclosingInstance() -
Method in class javafe.tc.EnvForLocals
- If there is an enclosing instance in scope, then return the
(exact) type of the innermost such instance.
- getEnclosingInstance() -
Method in class javafe.tc.EnvForTypeSig
- If there is an enclosing instance in scope, then return the
(exact) type of the innermost such instance.
- getEnclosingInstanceArg(ConstructorDecl) -
Static method in class escjava.translate.Inner
- * Return the FormalParaDecl for a given inner-class constructor's *
enclosing-instance-field argument (this$0arg).
- getEnclosingInstanceField(TypeSig) -
Static method in class escjava.translate.Inner
- * Return the FieldDecl for a given non-top-level TypeSig's * enclosing
instance field (this$0).
- getEndLoc() -
Method in class escjava.ast.AssignCmd
-
- getEndLoc() -
Method in class escjava.ast.Call
-
- getEndLoc() -
Method in class escjava.ast.CmdCmdCmd
-
- getEndLoc() -
Method in class escjava.ast.CondExprModifierPragma
-
- getEndLoc() -
Method in class escjava.ast.DecreasesInfo
-
- getEndLoc() -
Method in class escjava.ast.DependsPragma
-
- getEndLoc() -
Method in class escjava.ast.DynInstCmd
-
- getEndLoc() -
Method in class escjava.ast.ExprDeclPragma
-
- getEndLoc() -
Method in class escjava.ast.ExprModifierPragma
-
- getEndLoc() -
Method in class escjava.ast.ExprStmtPragma
-
- getEndLoc() -
Method in class escjava.ast.GCExpr
-
- getEndLoc() -
Method in class escjava.ast.GhostDeclPragma
-
- getEndLoc() -
Method in class escjava.ast.GuardExpr
-
- getEndLoc() -
Method in class escjava.ast.IdExprDeclPragma
-
- getEndLoc() -
Method in class escjava.ast.LoopCmd
-
- getEndLoc() -
Method in class escjava.ast.MapsExprModifierPragma
-
- getEndLoc() -
Method in class escjava.ast.ModelConstructorDeclPragma
-
- getEndLoc() -
Method in class escjava.ast.ModelDeclPragma
-
- getEndLoc() -
Method in class escjava.ast.ModelMethodDeclPragma
-
- getEndLoc() -
Method in class escjava.ast.ModelTypePragma
-
- getEndLoc() -
Method in class escjava.ast.NamedExprDeclPragma
-
- getEndLoc() -
Method in class escjava.ast.SeqCmd
-
- getEndLoc() -
Method in class escjava.ast.SetStmtPragma
-
- getEndLoc() -
Method in class escjava.ast.SkolemConstantPragma
-
- getEndLoc() -
Method in class escjava.ast.Spec
-
- getEndLoc() -
Method in class escjava.ast.VarExprModifierPragma
-
- getEndLoc() -
Method in class escjava.ast.VarInCmd
-
- getEndLoc() -
Method in class escjava.ast.WildRefExpr
-
- getEndLoc() -
Method in class javafe.ast.ASTNode
-
- getEndLoc() -
Method in class javafe.ast.AmbiguousMethodInvocation
-
- getEndLoc() -
Method in class javafe.ast.AmbiguousVariableAccess
-
- getEndLoc() -
Method in class javafe.ast.ArrayInit
-
- getEndLoc() -
Method in class javafe.ast.ArrayRefExpr
-
- getEndLoc() -
Method in class javafe.ast.ArrayType
-
- getEndLoc() -
Method in class javafe.ast.AssertStmt
-
- getEndLoc() -
Method in class javafe.ast.BinaryExpr
-
- getEndLoc() -
Method in class javafe.ast.CastExpr
-
- getEndLoc() -
Method in class javafe.ast.CatchClause
-
- getEndLoc() -
Method in class javafe.ast.ClassDeclStmt
-
- getEndLoc() -
Method in class javafe.ast.ClassLiteral
-
- getEndLoc() -
Method in class javafe.ast.CompilationUnit
-
- getEndLoc() -
Method in class javafe.ast.CondExpr
-
- getEndLoc() -
Method in class javafe.ast.ConstructorInvocation
-
- getEndLoc() -
Method in class javafe.ast.DoStmt
-
- getEndLoc() -
Method in class javafe.ast.EvalStmt
-
- getEndLoc() -
Method in class javafe.ast.FieldAccess
-
- getEndLoc() -
Method in class javafe.ast.FieldDecl
-
- getEndLoc() -
Method in class javafe.ast.ForStmt
-
- getEndLoc() -
Method in class javafe.ast.GenericBlockStmt
-
- getEndLoc() -
Method in class javafe.ast.GenericVarDecl
-
- getEndLoc() -
Method in class javafe.ast.IfStmt
-
- getEndLoc() -
Method in class javafe.ast.InitBlock
-
- getEndLoc() -
Method in class javafe.ast.InstanceOfExpr
-
- getEndLoc() -
Method in class javafe.ast.LabelStmt
-
- getEndLoc() -
Method in class javafe.ast.LiteralExpr
-
- getEndLoc() -
Method in class javafe.ast.LocalVarDecl
-
- getEndLoc() -
Method in class javafe.ast.MethodInvocation
-
- getEndLoc() -
Method in class javafe.ast.Name
- Override getEndLoc so it refers to the actual end of us.
- getEndLoc() -
Method in class javafe.ast.NewArrayExpr
-
- getEndLoc() -
Method in class javafe.ast.NewInstanceExpr
-
- getEndLoc() -
Method in class javafe.ast.ObjectDesignator
-
- getEndLoc() -
Method in class javafe.ast.ParenExpr
-
- getEndLoc() -
Method in class javafe.ast.ReturnStmt
-
- getEndLoc() -
Method in class javafe.ast.RoutineDecl
-
- getEndLoc() -
Method in class javafe.ast.SynchronizeStmt
-
- getEndLoc() -
Method in class javafe.ast.ThisExpr
-
- getEndLoc() -
Method in class javafe.ast.ThrowStmt
-
- getEndLoc() -
Method in class javafe.ast.TryCatchStmt
-
- getEndLoc() -
Method in class javafe.ast.TryFinallyStmt
-
- getEndLoc() -
Method in class javafe.ast.TypeDecl
-
- getEndLoc() -
Method in class javafe.ast.TypeName
-
- getEndLoc() -
Method in class javafe.ast.UnaryExpr
-
- getEndLoc() -
Method in class javafe.ast.VarDeclStmt
-
- getEndLoc() -
Method in class javafe.ast.WhileStmt
-
- getEndLoc() -
Method in class javafe.tc.TypeSig
-
- getEnv(boolean) -
Method in class javafe.tc.TypeSig
- Return an environment for use in checking code inside us.
- getEnvForCurrentSig(TypeSig, boolean) -
Method in class javafe.tc.PrepTypeDeclaration
-
- getEquivalentAxioms(RepHelper, Hashtable) -
Static method in class escjava.translate.TrAnExpr
-
- getExtension(String) -
Static method in class javafe.filespace.Extension
- Return the extension of a filename (including the ".") or "" if
it has none.
- getExternalName() -
Method in class javafe.tc.TypeSig
- Return our exact fully-qualified external name as a
human-readable string suitable for display.
- getFields(boolean) -
Method in class escjava.tc.GhostEnv
-
- getFields(boolean) -
Method in class javafe.tc.EnvForTypeSig
-
- getFields(boolean) -
Method in class javafe.tc.TypeSig
- Returns all fields of the type declaration associated with
this, including inherited ones.
- getFieldsRaw() -
Method in class javafe.tc.TypeSig
-
- getFile() -
Method in class javafe.util.CorrelatedReader
- Returns the file underlying this correlated reader.
- getFile(int) -
Static method in class javafe.util.ErrorSet
- Return a new InputStream for the file that loc refers to or null
if an I/O error occurs while attempting to open the stream.
- getFile() -
Method in class javafe.util.FileCorrelatedReader
- Returns the file underlying this correlated reader.
- getFile() -
Method in class javafe.util.FilterCorrelatedReader
- Returns the file underlying this correlated reader.
- getFile() -
Method in class javafe.util.SubCorrelatedReader
- Returns the file underlying this correlated reader.
- getFilename() -
Method in class escjava.gui.GUI.EscTreeValue
-
- getFilename() -
Method in class escjava.gui.GUI.GFCUTreeValue
-
- getFilename() -
Method in class escjava.gui.GUI.IETreeValue
-
- getFilename() -
Method in class escjava.gui.GUI.RDTreeValue
-
- getFilename() -
Method in class escjava.gui.GUI.TDTreeValue
-
- getFirstInheritedInterfaces(ClassDecl) -
Static method in class escjava.translate.GetSpec
-
- getFloatConstant(Object) -
Static method in class javafe.tc.ConstantExpr
-
- getFormalParaTypes(FormalParaDeclVec) -
Static method in class javafe.tc.Types
-
- getFreeVars() -
Method in class escjava.translate.CalcFreeVars
-
- getGCTagForBinary(BinaryExpr) -
Static method in class escjava.translate.TrAnExpr
-
- getGCTagForUnary(UnaryExpr) -
Static method in class escjava.translate.TrAnExpr
- TBW.
- getGhostField(String, FieldDecl) -
Method in class escjava.tc.GhostEnv
- Attempts to find a ghost or model field that belongs
to us (including supertypes) with
name
n that is not equal to excluded, which may
be null.
- getHiddenFields() -
Method in class javafe.tc.TypeSig
-
- getHumanName() -
Method in interface javafe.genericfile.GenericFile
- Return a name that uniquely identifies us to the user.
- getHumanName() -
Method in class javafe.genericfile.NormalGenericFile
-
- getHumanName() -
Method in class javafe.genericfile.UnopenableFile
- *
GenericFile interface implementation: *
*
- getHumanName() -
Method in class javafe.genericfile.ZipGenericFile
- Return a name that uniquely identifies us to the user.
- getId() -
Method in class escjava.ast.DerivedMethodDecl
-
- getImplementsSet(ClassDecl, MethodDecl) -
Method in class javafe.tc.TypeCheck
- Retrieves the set of interface
MethodDecls that a given
class MethodDecl implements.
- getImplementsSet(MethodDecl) -
Method in class javafe.tc.TypeCheck
- Retrieves the set of interface
MethodDecls that a
given interface MethodDecl implements.
- getInferredThisExpr(TypeSig, int) -
Method in class javafe.tc.Env
- Return an inferred ThisExpr for "[C.]this", using location loc.
- getInfoNewTree() -
Method in class javafe.ast.LiteralExpr
-
- getInheritedSpecs(RoutineDecl) -
Static method in class escjava.ast.Utils
-
- getInitVar(GenericVarDecl) -
Static method in class escjava.translate.Translate
- Return the
VariableAccesss associated with d by a
call to setInitVar.
- getInitialState() -
Method in class escjava.translate.InitialState
-
- getInnermostInstance() -
Method in class javafe.tc.Env
- Returns the innermost current or enclosing instance, or null
if none exists.
- getInputStream() -
Method in interface javafe.genericfile.GenericFile
- Open the file we represent as an InputStream.
- getInputStream() -
Method in class javafe.genericfile.NormalGenericFile
- Open the file we represent as an
InputStream.
- getInputStream() -
Method in class javafe.genericfile.UnopenableFile
-
- getInputStream() -
Method in class javafe.genericfile.ZipGenericFile
- Open the file we represent as an InputStream.
- getInst() -
Static method in class javafe.tc.PrepTypeDeclaration
-
- getInstance() -
Static method in class escjava.Main
-
- getIntConstant(Object) -
Static method in class javafe.tc.ConstantExpr
-
- getInteger() -
Method in class escjava.prover.SExp
- If we represent an integer, return it as an
int;
otherwise, throw an SExpTypeError.
- getInteger() -
Method in class escjava.prover.SInt
- If we represent an integer, return it as an
int;
otherwise, throw SExpTypeError.
- getJavaLang(String) -
Static method in class javafe.tc.Types
- Find the TypeSig for the required package-member type
java.lang.T.
- getJavaModifier(Lex, int) -
Method in class javafe.parser.ParseUtil
- Checks if the next token is a Java modifier.
- getKey(String[], String) -
Static method in class javafe.tc.TypeSig
- Compute the key for map for fully-qualified type P.T.
- getKind() -
Method in class escjava.prover.SimplifyOutput
-
- getLabel() -
Method in class javafe.filespace.Tree
- Return the label on the edge to us from our parent or null if we
have no parent.
- getLabels() -
Method in class escjava.prover.SimplifyResult
-
- getLexicalPragmas() -
Method in class javafe.parser.Lex
- Returns the set of lexical pragmas collected.
- getLine() -
Method in class escjava.gui.GUI.EscTreeValue
-
- getLine() -
Method in class escjava.gui.GUI.GFCUTreeValue
-
- getLine() -
Method in class escjava.gui.GUI.IETreeValue
-
- getLine() -
Method in class escjava.gui.GUI.RDTreeValue
-
- getLine() -
Method in class escjava.gui.GUI.TDTreeValue
-
- getLine(int) -
Static method in class javafe.util.ErrorSet
- Return the line loc refers to or null if an I/O error occurs
while attempting to read the line in.
- getList() -
Method in class escjava.prover.SExp
- If we represent a list, return it as an
SList;
otherwise, throw SExpTypeError.
- getList() -
Method in class escjava.prover.SList
-
- getLoc(String, int) -
Static method in class escjava.translate.ErrorMsg
- Converts string
s, beginning at index k,
into a location.
- getLocalName() -
Method in interface javafe.genericfile.GenericFile
- Return our local name, the name that distinguishes us
within the directory that contains us.
- getLocalName() -
Method in class javafe.genericfile.NormalGenericFile
-
- getLocalName() -
Method in class javafe.genericfile.UnopenableFile
-
- getLocalName() -
Method in class javafe.genericfile.ZipGenericFile
- Return our local name, the name that distinguishes us
within the directory that contains us.
- getLocation() -
Method in class escjava.parser.JmlCorrelatedReader
-
- getLocation() -
Method in class escjava.prover.TriggerlessQuantWarning
- Attempts to glean a location from the name of the dummy
variable appearing in
e1.
- getLocation() -
Method in class javafe.util.BufferedCorrelatedReader
- Returns the location of the last character read.
- getLocation() -
Method in class javafe.util.CorrelatedReader
- Returns the location of the last character read.
- getLocation() -
Method in class javafe.util.FilterCorrelatedReader
- Returns the location of the last character read.
- getLongConstant(Object) -
Static method in class javafe.tc.ConstantExpr
-
- getMap(TypeDecl) -
Static method in class escjava.tc.Datagroups
-
- getMethods() -
Method in class javafe.tc.TypeSig
- Similar to
getFields, except for methods.
- getModelVarAxioms(TypeDecl, FieldDecl, Hashtable) -
Static method in class escjava.translate.TrAnExpr
-
- getModifiers() -
Method in class escjava.ast.ExprDeclPragma
-
- getModifiers() -
Method in class escjava.ast.IdExprDeclPragma
-
- getModifiers() -
Method in class escjava.ast.NamedExprDeclPragma
-
- getModifiers() -
Method in class javafe.ast.GenericVarDecl
-
- getModifiers() -
Method in class javafe.ast.InitBlock
-
- getModifiers() -
Method in class javafe.ast.RoutineDecl
-
- getModifiers() -
Method in class javafe.ast.TypeDecl
-
- getModifiers() -
Method in interface javafe.ast.TypeDeclElem
-
- getModifiers() -
Method in class javafe.ast.TypeDeclElemPragma
-
- getMsg() -
Method in class escjava.prover.SimplifyComment
-
- getName() -
Method in class escjava.vcGeneration.TMethodCall
- return the VariableInfo associated with the method name,
of interest for the return type of the method.
- getName(RoutineDecl) -
Method in class javafe.tc.TypeCheck
- Returns the user-readable name for a
RoutineDecl.
- getNameASTNode(ASTNode) -
Static method in class escjava.vcGeneration.VcGenerator
- Utility method for creating dot representation of gc tree
- getNameQualifier(Name) -
Static method in class javafe.reader.ASTClassFileParser
- Return the package qualifier of a given name.
- getNameTerminal(Name) -
Static method in class javafe.reader.ASTClassFileParser
- Return the terminal identifier of a given name.
- getNext() -
Method in class escjava.pa.generic.EnumKofN
-
- getNextPragma(Token) -
Method in class escjava.parser.ErrorPragmaParser
- Produce no actual pragmas.
- getNextPragma(Token) -
Method in class escjava.parser.EscPragmaParser
- Parse the next pragma, putting information about it in the provided token
dst, and return a flag indicating if there are further pragmas to
be parsed.
- getNextPragma(Token) -
Method in interface javafe.parser.PragmaParser
- Parse the next pragma.
- getNextPragmaHelper(Token) -
Method in class escjava.parser.EscPragmaParser
-
- getNextToken() -
Method in class javafe.parser.Lex
- Scans next token from input stream.
- getNil() -
Static method in class escjava.prover.SNil
-
- getNonNullAndNullable(RoutineDecl) -
Method in class escjava.AnnotationHandler
- Find every formal parameter or reslut of a routine declaration
that is either non_null or nullable.
- getObjectDecl() -
Method in class escjava.RefinementSequence
-
- getObjectDesignator(TypeSig, int) -
Method in class javafe.tc.Env
- Return an inferred ObjectDesignator for use in a reference to
a possibly-instance member of class C from here.
- getOriginalMethod(MethodDecl) -
Static method in class escjava.translate.Suggestion
- Returns a method that
md overrides.
- getOverrideStatus(RoutineDecl) -
Static method in class escjava.tc.FlowInsensitiveChecks
-
- getOverrides(MethodDecl) -
Method in class javafe.tc.PrepTypeDeclaration
- 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.
- getOverrides(TypeDecl, MethodDecl) -
Method in class javafe.tc.PrepTypeDeclaration
- Returns the set of methods that
md overrides, with
md considered to appear in a particular type
td.
- getOverrides(MethodDecl) -
Method in class javafe.tc.TypeCheck
- Retrieves the class
MethodDecl that a given class
MethodDecl overrides.
- getPModifiers() -
Method in class escjava.ast.GhostDeclPragma
-
- getPModifiers() -
Method in class escjava.ast.ModelDeclPragma
-
- getPModifiers() -
Method in class javafe.ast.FieldDecl
-
- getPModifiers() -
Method in class javafe.ast.InitBlock
-
- getPModifiers() -
Method in class javafe.ast.RoutineDecl
-
- getPModifiers() -
Method in class javafe.ast.TypeDecl
-
- getPModifiers() -
Method in interface javafe.ast.TypeDeclElem
-
- getPModifiers() -
Method in class javafe.ast.TypeDeclElemPragma
-
- getPackage(String[]) -
Method in class javafe.filespace.SlowQuery
-
- getPackageName(Tree) -
Static method in class javafe.filespace.PkgTree
- Return the human-readable name of a package.
- getPackageName() -
Method in class javafe.tc.TypeSig
- Return our package name as a human-readable string
suitable for display.
- getPair() -
Method in class escjava.prover.SList
- If we represent a non-empty list, return it as a
SPair; otherwise, throw SExpTypeError.
- getPair() -
Method in class escjava.prover.SPair
- If we represent a non-empty list, return it as a
SPair; otherwise, throw SExpTypeError.
- getParent() -
Method in class escjava.gui.GUI.EscTreeValue
-
- getParent() -
Method in class javafe.ast.FieldDecl
-
- getParent() -
Method in class javafe.ast.InitBlock
-
- getParent() -
Method in class javafe.ast.RoutineDecl
-
- getParent() -
Method in class javafe.ast.TypeDecl
-
- getParent() -
Method in interface javafe.ast.TypeDeclElem
- The TypeDecl we are an element of, or null if we do not have a
parent (cf. hasParent).
- getParent() -
Method in class javafe.ast.TypeDeclElemPragma
-
- getParent() -
Method in class javafe.filespace.Tree
- Return our parent node or null if we have no parent
- getPragma(Token) -
Method in class escjava.parser.EscPragmaParser
-
- getPreMap() -
Method in class escjava.translate.InitialState
-
- getProof(Writer, String, TNode) -
Method in class escjava.vcGeneration.ProverType
- This method allows a VC term (generated by using the visitor pattern), for
example, to:
be wrapped up as a prover assertion (eg. a lemma or theorem for the prover)
universally quantify all free variables in the VC term
- getProof(Writer, String) -
Method in class escjava.vcGeneration.VcGenerator
-
- getProof(Writer, String, TNode) -
Method in class escjava.vcGeneration.coq.CoqProver
-
- getProof(Writer, String, TNode) -
Method in class escjava.vcGeneration.pvs.PvsProver
-
- getProof(Writer, String, TNode) -
Method in class escjava.vcGeneration.sammy.SammyProver
-
- getProof(Writer, String, TNode) -
Method in class escjava.vcGeneration.simplify.SimplifyProver
-
- getProof(Writer, String, TNode) -
Method in class escjava.vcGeneration.xml.XmlProver
- Here we ensure that the resulting XML term is suitable for writing to an output file.
- getQualifiedChild(String, char) -
Method in class javafe.filespace.Tree
- Return the child with a given partially qualified name or null
if no such node exists; if this node is X.Y and name is Z!
- getQualifiedName(String) -
Method in class javafe.filespace.Tree
- Return a fully qualified name for this node using a specified
separator String.
- getRawSig(TypeName) -
Method in class javafe.tc.TypeCheck
-
- getRawSig(TypeName) -
Static method in class javafe.tc.TypeSig
- Gets the TypeSig recorded by
setSig, or null.
- getRefinementSequence(String[], Identifier, CompilationUnit, boolean) -
Method in class escjava.reader.RefinementCachedReader
-
- getReplacementCount() -
Static method in class escjava.translate.TrAnExpr
- Returns the number of variable substitutions that calls to
trSpecExpr have caused.
- getReporter() -
Static method in class javafe.util.ErrorSet
- Returns the current output reporter.
- getRepresentsAxiom(NamedExprDeclPragma, Hashtable) -
Static method in class escjava.translate.TrAnExpr
- Translates an individual represents clause into a class-level axiom.
- getRepresentsClauses(TypeDecl, FieldDecl) -
Static method in class escjava.translate.GetSpec
- Gets the represents clauses for a model field fd as seen from a type
declaration td; fd may be declared in td or in a supertype of td.
- getReturn() -
Method in class javafe.reader.MethodSignature
- Return the return type of this method signature.
- getRootInterface() -
Method in class escjava.tc.PrepTypeDeclaration
-
- getRootInterface() -
Method in class javafe.tc.PrepTypeDeclaration
- This routine constructs and returns the interface that all
interfaces are de-facto subinterfaces of.
- getRootNode() -
Method in class javafe.filespace.Tree
- Return the root node for the tree we belong to.
- getRoutineDeclEndLoc() -
Method in class escjava.ast.DerivedMethodDecl
-
- getRoutineDeclStartLoc() -
Method in class escjava.ast.DerivedMethodDecl
-
- getRoutineName(RoutineDecl) -
Method in class javafe.tc.TypeCheck
- Returns the user-readable simple name for a
RoutineDecl.
- getSecondType() -
Method in class escjava.vcGeneration.VariableInfo
-
- getShortName() -
Method in class escjava.vcGeneration.TNode
-
- getSibling(String) -
Method in interface javafe.genericfile.GenericFile
- Attempt to return a GenericFile that describes the file in the
same "directory" as us that has the local name
n.
- getSibling(String) -
Method in class javafe.genericfile.NormalGenericFile
-
- getSibling(String) -
Method in class javafe.genericfile.UnopenableFile
-
- getSibling(String) -
Method in class javafe.genericfile.ZipGenericFile
- Attempt to return a GenericFile that describes the file in the
same "directory" as us that has the local name
n.
- getSig(TypeDecl) -
Method in class javafe.tc.TypeCheck
- Retrieves the
TypeSig associated with a particular
TypeDecl.
- getSig(TypeName) -
Method in class javafe.tc.TypeCheck
- Retrieves the
TypeSig associated with a particular
TypeName.
- getSig(TypeDecl) -
Static method in class javafe.tc.TypeSig
- The myTypeDecl field maps TypeSigs to TypeDecls.
- getSig(TypeName) -
Static method in class javafe.tc.TypeSig
- Gets the TypeSig recorded by
setSig.
- getSignature(RoutineDecl) -
Static method in class javafe.tc.TypeCheck
- Construct a
String listing the signature of a
RoutineDecl, omitting the return type and throws
causes if any.
- getSimpleName() -
Method in class javafe.filespace.Tree
- The same as getLabel, except that it returns "" instead of null
for the top node.
- getSortedChildren(Tree) -
Static method in class javafe.filespace.TreeWalker
- Return a sorted list of a Tree's direct children:
- getSpecForBody(RoutineDecl, FindContributors, Set, Hashtable) -
Static method in class escjava.translate.GetSpec
-
- getSpecForCall(RoutineDecl, FindContributors, Set) -
Static method in class escjava.translate.GetSpec
-
- getSpecForInline(RoutineDecl, FindContributors) -
Static method in class escjava.translate.GetSpec
-
- getSpecForInline -
Variable in class escjava.translate.InlineSettings
-
- getStartLoc() -
Method in class escjava.ast.ArrayRangeRefExpr
-
- getStartLoc() -
Method in class escjava.ast.AssignCmd
-
- getStartLoc() -
Method in class escjava.ast.Call
-
- getStartLoc() -
Method in class escjava.ast.CmdCmdCmd
-
- getStartLoc() -
Method in class escjava.ast.CondExprModifierPragma
-
- getStartLoc() -
Method in class escjava.ast.Condition
-
- getStartLoc() -
Method in class escjava.ast.DecreasesInfo
-
- getStartLoc() -
Method in class escjava.ast.DefPred
-
- getStartLoc() -
Method in class escjava.ast.DefPredApplExpr
-
- getStartLoc() -
Method in class escjava.ast.DefPredLetExpr
-
- getStartLoc() -
Method in class escjava.ast.DependsPragma
-
- getStartLoc() -
Method in class escjava.ast.DynInstCmd
-
- getStartLoc() -
Method in class escjava.ast.EverythingExpr
-
- getStartLoc() -
Method in class escjava.ast.ExprCmd
-
- getStartLoc() -
Method in class escjava.ast.ExprDeclPragma
-
- getStartLoc() -
Method in class escjava.ast.ExprModifierPragma
-
- getStartLoc() -
Method in class escjava.ast.ExprStmtPragma
-
- getStartLoc() -
Method in class escjava.ast.GCExpr
-
- getStartLoc() -
Method in class escjava.ast.GhostDeclPragma
-
- getStartLoc() -
Method in class escjava.ast.GuardExpr
-
- getStartLoc() -
Method in class escjava.ast.IdExprDeclPragma
-
- getStartLoc() -
Method in class escjava.ast.IdentifierModifierPragma
-
- getStartLoc() -
Method in class escjava.ast.ImportPragma
-
- getStartLoc() -
Method in class escjava.ast.LockSetExpr
-
- getStartLoc() -
Method in class escjava.ast.LoopCmd
-
- getStartLoc() -
Method in class escjava.ast.MapsExprModifierPragma
-
- getStartLoc() -
Method in class escjava.ast.ModelConstructorDeclPragma
-
- getStartLoc() -
Method in class escjava.ast.ModelDeclPragma
-
- getStartLoc() -
Method in class escjava.ast.ModelMethodDeclPragma
-
- getStartLoc() -
Method in class escjava.ast.ModelProgamModifierPragma
-
- getStartLoc() -
Method in class escjava.ast.ModelTypePragma
-
- getStartLoc() -
Method in class escjava.ast.ModifiesGroupPragma
-
- getStartLoc() -
Method in class escjava.ast.NamedExprDeclPragma
-
- getStartLoc() -
Method in class escjava.ast.NestedModifierPragma
-
- getStartLoc() -
Method in class escjava.ast.NotModifiedExpr
-
- getStartLoc() -
Method in class escjava.ast.NotSpecifiedExpr
-
- getStartLoc() -
Method in class escjava.ast.NothingExpr
-
- getStartLoc() -
Method in class escjava.ast.NowarnPragma
-
- getStartLoc() -
Method in class escjava.ast.ParsedSpecs
-
- getStartLoc() -
Method in class escjava.ast.ReachModifierPragma
-
- getStartLoc() -
Method in class escjava.ast.RefinePragma
-
- getStartLoc() -
Method in class escjava.ast.ResExpr
-
- getStartLoc() -
Method in class escjava.ast.SeqCmd
-
- getStartLoc() -
Method in class escjava.ast.SetCompExpr
-
- getStartLoc() -
Method in class escjava.ast.SetStmtPragma
-
- getStartLoc() -
Method in class escjava.ast.SimpleCmd
-
- getStartLoc() -
Method in class escjava.ast.SimpleModifierPragma
-
- getStartLoc() -
Method in class escjava.ast.SimpleStmtPragma
-
- getStartLoc() -
Method in class escjava.ast.SkolemConstantPragma
-
- getStartLoc() -
Method in class escjava.ast.Spec
-
- getStartLoc() -
Method in class escjava.ast.StillDeferredDeclPragma
-
- getStartLoc() -
Method in class escjava.ast.VarDeclModifierPragma
-
- getStartLoc() -
Method in class escjava.ast.VarExprModifierPragma
-
- getStartLoc() -
Method in class escjava.ast.VarInCmd
-
- getStartLoc() -
Method in class escjava.ast.WildRefExpr
-
- getStartLoc() -
Method in class javafe.ast.ASTNode
-
- getStartLoc() -
Method in class javafe.ast.AmbiguousMethodInvocation
-
- getStartLoc() -
Method in class javafe.ast.AmbiguousVariableAccess
-
- getStartLoc() -
Method in class javafe.ast.ArrayInit
-
- getStartLoc() -
Method in class javafe.ast.ArrayRefExpr
-
- getStartLoc() -
Method in class javafe.ast.ArrayType
-
- getStartLoc() -
Method in class javafe.ast.AssertStmt
-
- getStartLoc() -
Method in class javafe.ast.BinaryExpr
-
- getStartLoc() -
Method in class javafe.ast.BlockStmt
-
- getStartLoc() -
Method in class javafe.ast.BranchStmt
-
- getStartLoc() -
Method in class javafe.ast.CastExpr
-
- getStartLoc() -
Method in class javafe.ast.CatchClause
-
- getStartLoc() -
Method in class javafe.ast.ClassDeclStmt
-
- getStartLoc() -
Method in class javafe.ast.ClassLiteral
-
- getStartLoc() -
Method in class javafe.ast.CompilationUnit
-
- getStartLoc() -
Method in class javafe.ast.CompoundName
-
- getStartLoc() -
Method in class javafe.ast.CondExpr
-
- getStartLoc() -
Method in class javafe.ast.ConstructorInvocation
-
- getStartLoc() -
Method in class javafe.ast.DoStmt
-
- getStartLoc() -
Method in class javafe.ast.ErrorType
-
- getStartLoc() -
Method in class javafe.ast.EvalStmt
-
- getStartLoc() -
Method in class javafe.ast.ExprObjectDesignator
-
- getStartLoc() -
Method in class javafe.ast.FieldAccess
-
- getStartLoc() -
Method in class javafe.ast.ForStmt
-
- getStartLoc() -
Method in class javafe.ast.GenericVarDecl
-
- getStartLoc() -
Method in class javafe.ast.IdentifierNode
-
- getStartLoc() -
Method in class javafe.ast.IfStmt
-
- getStartLoc() -
Method in class javafe.ast.ImportDecl
-
- getStartLoc() -
Method in class javafe.ast.InitBlock
-
- getStartLoc() -
Method in class javafe.ast.InstanceOfExpr
-
- getStartLoc() -
Method in class javafe.ast.LabelStmt
-
- getStartLoc() -
Method in class javafe.ast.LiteralExpr
-
- getStartLoc() -
Method in class javafe.ast.MethodInvocation
-
- getStartLoc() -
Method in class javafe.ast.NewArrayExpr
-
- getStartLoc() -
Method in class javafe.ast.NewInstanceExpr
-
- getStartLoc() -
Method in class javafe.ast.ParenExpr
-
- getStartLoc() -
Method in class javafe.ast.PrimitiveType
-
- getStartLoc() -
Method in class javafe.ast.ReturnStmt
-
- getStartLoc() -
Method in class javafe.ast.RoutineDecl
-
- getStartLoc() -
Method in class javafe.ast.SimpleName
-
- getStartLoc() -
Method in class javafe.ast.SkipStmt
-
- getStartLoc() -
Method in class javafe.ast.SuperObjectDesignator
-
- getStartLoc() -
Method in class javafe.ast.SwitchLabel
-
- getStartLoc() -
Method in class javafe.ast.SwitchStmt
-
- getStartLoc() -
Method in class javafe.ast.SynchronizeStmt
-
- getStartLoc() -
Method in class javafe.ast.ThisExpr
-
- getStartLoc() -
Method in class javafe.ast.ThrowStmt
-
- getStartLoc() -
Method in class javafe.ast.TryCatchStmt
-
- getStartLoc() -
Method in class javafe.ast.TryFinallyStmt
-
- getStartLoc() -
Method in class javafe.ast.TypeDecl
-
- getStartLoc() -
Method in interface javafe.ast.TypeDeclElem
-
- getStartLoc() -
Method in class javafe.ast.TypeName
-
- getStartLoc() -
Method in class javafe.ast.TypeObjectDesignator
-
- getStartLoc() -
Method in class javafe.ast.UnaryExpr
-
- getStartLoc() -
Method in class javafe.ast.VarDeclStmt
-
- getStartLoc() -
Method in class javafe.ast.VariableAccess
-
- getStartLoc() -
Method in class javafe.ast.WhileStmt
-
- getStartLoc() -
Method in class javafe.tc.TypeSig
-
- getStatus(Tree) -
Static method in class javafe.filespace.PkgTree
- Decide what to do with a node of the underlying filespace, returning
one of the following codes: IGNORE, INCLUDE_NODE, or INCLUDE_TREE.
- getStatusText() -
Method in class escjava.gui.GUI.EscTreeValue
-
- getString(int) -
Static method in class javafe.parser.TagConstants
-
- getSuperClass(TypeDecl) -
Method in class javafe.TestTool
- Attempt to fetch the
TypeSig for a given
TypeDecl.
- getSuperClassOverride(MethodDecl) -
Static method in class escjava.tc.FlowInsensitiveChecks
-
- getSuperNonNullStatus(RoutineDecl, int) -
Static method in class escjava.tc.FlowInsensitiveChecks
-
- getSuperNonNullStatus(RoutineDecl, int, Set) -
Static method in class escjava.tc.FlowInsensitiveChecks
-
- getTag() -
Method in class escjava.ast.AnOverview
- Return the tag of a node.
- getTag() -
Method in class escjava.ast.ArrayRangeRefExpr
-
- getTag() -
Method in class escjava.ast.Call
-
- getTag() -
Method in class escjava.ast.CmdCmdCmd
-
- getTag() -
Method in class escjava.ast.CondExprModifierPragma
-
- getTag() -
Method in class escjava.ast.Condition
-
- getTag() -
Method in class escjava.ast.DecreasesInfo
-
- getTag() -
Method in class escjava.ast.DefPred
-
- getTag() -
Method in class escjava.ast.DefPredApplExpr
-
- getTag() -
Method in class escjava.ast.DefPredLetExpr
-
- getTag() -
Method in class escjava.ast.DependsPragma
-
- getTag() -
Method in class escjava.ast.DynInstCmd
-
- getTag() -
Method in class escjava.ast.EverythingExpr
-
- getTag() -
Method in class escjava.ast.ExprCmd
-
- getTag() -
Method in class escjava.ast.ExprDeclPragma
-
- getTag() -
Method in class escjava.ast.ExprModifierPragma
-
- getTag() -
Method in class escjava.ast.ExprStmtPragma
-
- getTag() -
Method in class escjava.ast.GCExpr
- Return the tag of a node.
- getTag() -
Method in class escjava.ast.GeneralizedQuantifiedExpr
-
- getTag() -
Method in class escjava.ast.GetsCmd
-
- getTag() -
Method in class escjava.ast.GhostDeclPragma
-
- getTag() -
Method in class escjava.ast.GuardExpr
-
- getTag() -
Method in class escjava.ast.GuardedCmd
- Return the tag of a node.
- getTag() -
Method in class escjava.ast.IdExprDeclPragma
-
- getTag() -
Method in class escjava.ast.IdentifierModifierPragma
-
- getTag() -
Method in class escjava.ast.ImportPragma
-
- getTag() -
Method in class escjava.ast.LabelExpr
-
- getTag() -
Method in class escjava.ast.LockSetExpr
-
- getTag() -
Method in class escjava.ast.LoopCmd
-
- getTag() -
Method in class escjava.ast.MapsExprModifierPragma
-
- getTag() -
Method in class escjava.ast.ModelConstructorDeclPragma
-
- getTag() -
Method in class escjava.ast.ModelDeclPragma
-
- getTag() -
Method in class escjava.ast.ModelMethodDeclPragma
-
- getTag() -
Method in class escjava.ast.ModelProgamModifierPragma
-
- getTag() -
Method in class escjava.ast.ModelTypePragma
-
- getTag() -
Method in class escjava.ast.ModifiesGroupPragma
-
- getTag() -
Method in class escjava.ast.NamedExprDeclPragma
-
- getTag() -
Method in class escjava.ast.NaryExpr
-
- getTag() -
Method in class escjava.ast.NestedModifierPragma
-
- getTag() -
Method in class escjava.ast.NotModifiedExpr
-
- getTag() -
Method in class escjava.ast.NotSpecifiedExpr
-
- getTag() -
Method in class escjava.ast.NothingExpr
-
- getTag() -
Method in class escjava.ast.NowarnPragma
-
- getTag() -
Method in class escjava.ast.NumericalQuantifiedExpr
-
- getTag() -
Method in class escjava.ast.ParsedSpecs
-
- getTag() -
Method in class escjava.ast.QuantifiedExpr
-
- getTag() -
Method in class escjava.ast.ReachModifierPragma
-
- getTag() -
Method in class escjava.ast.RefinePragma
-
- getTag() -
Method in class escjava.ast.ResExpr
-
- getTag() -
Method in class escjava.ast.RestoreFromCmd
-
- getTag() -
Method in class escjava.ast.SeqCmd
-
- getTag() -
Method in class escjava.ast.SetCompExpr
-
- getTag() -
Method in class escjava.ast.SetStmtPragma
-
- getTag() -
Method in class escjava.ast.SimpleCmd
-
- getTag() -
Method in class escjava.ast.SimpleModifierPragma
-
- getTag() -
Method in class escjava.ast.SimpleStmtPragma
-
- getTag() -
Method in class escjava.ast.SkolemConstantPragma
-
- getTag() -
Method in class escjava.ast.Spec
-
- getTag() -
Method in class escjava.ast.StillDeferredDeclPragma
-
- getTag() -
Method in class escjava.ast.SubGetsCmd
-
- getTag() -
Method in class escjava.ast.SubSubGetsCmd
-
- getTag() -
Method in class escjava.ast.SubstExpr
-
- getTag() -
Method in class escjava.ast.TypeExpr
-
- getTag() -
Method in class escjava.ast.VarDeclModifierPragma
-
- getTag() -
Method in class escjava.ast.VarExprModifierPragma
-
- getTag() -
Method in class escjava.ast.VarInCmd
-
- getTag() -
Method in class escjava.ast.WildRefExpr
-
- getTag() -
Method in class javafe.ast.ASTNode
- Return the tag of a node.
- getTag() -
Method in class javafe.ast.AmbiguousMethodInvocation
-
- getTag() -
Method in class javafe.ast.AmbiguousVariableAccess
-
- getTag() -
Method in class javafe.ast.ArrayInit
-
- getTag() -
Method in class javafe.ast.ArrayRefExpr
-
- getTag() -
Method in class javafe.ast.ArrayType
-
- getTag() -
Method in class javafe.ast.AssertStmt
-
- getTag() -
Method in class javafe.ast.BinaryExpr
-
- getTag() -
Method in class javafe.ast.BlockStmt
-
- getTag() -
Method in class javafe.ast.BreakStmt
-
- getTag() -
Method in class javafe.ast.CastExpr
-
- getTag() -
Method in class javafe.ast.CatchClause
-
- getTag() -
Method in class javafe.ast.ClassDecl
-
- getTag() -
Method in class javafe.ast.ClassDeclStmt
-
- getTag() -
Method in class javafe.ast.ClassLiteral
-
- getTag() -
Method in class javafe.ast.CompilationUnit
-
- getTag() -
Method in class javafe.ast.CompoundName
-
- getTag() -
Method in class javafe.ast.CondExpr
-
- getTag() -
Method in class javafe.ast.ConstructorDecl
-
- getTag() -
Method in class javafe.ast.ConstructorInvocation
-
- getTag() -
Method in class javafe.ast.ContinueStmt
-
- getTag() -
Method in class javafe.ast.DoStmt
-
- getTag() -
Method in class javafe.ast.ErrorType
-
- getTag() -
Method in class javafe.ast.EvalStmt
-
- getTag() -
Method in class javafe.ast.ExprObjectDesignator
-
- getTag() -
Method in class javafe.ast.FieldAccess
-
- getTag() -
Method in class javafe.ast.FieldDecl
-
- getTag() -
Method in class javafe.ast.ForStmt
-
- getTag() -
Method in class javafe.ast.FormalParaDecl
-
- getTag() -
Method in class javafe.ast.IdentifierNode
-
- getTag() -
Method in class javafe.ast.IfStmt
-
- getTag() -
Method in class javafe.ast.InitBlock
-
- getTag() -
Method in class javafe.ast.InstanceOfExpr
-
- getTag() -
Method in class javafe.ast.InterfaceDecl
-
- getTag() -
Method in class javafe.ast.LabelStmt
-
- getTag() -
Method in class javafe.ast.LiteralExpr
-
- getTag() -
Method in class javafe.ast.LocalVarDecl
-
- getTag() -
Method in class javafe.ast.MethodDecl
-
- getTag() -
Method in class javafe.ast.MethodInvocation
-
- getTag() -
Method in class javafe.ast.NewArrayExpr
-
- getTag() -
Method in class javafe.ast.NewInstanceExpr
-
- getTag() -
Method in class javafe.ast.OnDemandImportDecl
-
- getTag() -
Method in class javafe.ast.ParenExpr
-
- getTag() -
Method in class javafe.ast.PrimitiveType
-
- getTag() -
Method in class javafe.ast.ReturnStmt
-
- getTag() -
Method in class javafe.ast.SimpleName
-
- getTag() -
Method in class javafe.ast.SingleTypeImportDecl
-
- getTag() -
Method in class javafe.ast.SkipStmt
-
- getTag() -
Method in class javafe.ast.SuperObjectDesignator
-
- getTag() -
Method in class javafe.ast.SwitchLabel
-
- getTag() -
Method in class javafe.ast.SwitchStmt
-
- getTag() -
Method in class javafe.ast.SynchronizeStmt
-
- getTag() -
Method in class javafe.ast.ThisExpr
-
- getTag() -
Method in class javafe.ast.ThrowStmt
-
- getTag() -
Method in class javafe.ast.TryCatchStmt
-
- getTag() -
Method in class javafe.ast.TryFinallyStmt
-
- getTag() -
Method in interface javafe.ast.TypeDeclElem
- Return the tag of a node.
- getTag() -
Method in class javafe.ast.TypeDeclElemPragma
-
- getTag() -
Method in class javafe.ast.TypeName
-
- getTag() -
Method in class javafe.ast.TypeObjectDesignator
-
- getTag() -
Method in class javafe.ast.UnaryExpr
-
- getTag() -
Method in class javafe.ast.VarDeclStmt
-
- getTag() -
Method in class javafe.ast.VariableAccess
-
- getTag() -
Method in class javafe.ast.WhileStmt
-
- getTag() -
Method in class javafe.tc.TypeSig
-
- getTask() -
Method in class escjava.gui.TaskQueue
-
- getTask() -
Static method in class escjava.gui.WindowTasks
-
- getTokenType(Identifier) -
Static method in class javafe.ast._SpecialParserInterface
- Return the hidden "token type" field of
id.
- getTreeCellRendererComponent(JTree, Object, boolean, boolean, boolean, int, boolean) -
Method in class escjava.gui.EscFrame.EscRenderer
-
- getTreeCellRendererComponent(JTree, Object, boolean, boolean, boolean, int, boolean) -
Method in class escjava.gui.EscFrame.EscTreeCellRenderer
-
- getType() -
Method in class escjava.vcGeneration.TNode
- return the type of the node according to the type of proof asked
or "?"
- getType(VarInit) -
Static method in class javafe.tc.FlowInsensitiveChecks
- Retrieves the
Type of a VarInit.
- getType(VarInit) -
Method in class javafe.tc.TypeCheck
- Retrieves the
Type of a VarInit.
- getTypeDecl() -
Method in class javafe.tc.TypeSig
- Get the non-null TypeDecl we are associated with.
- getTypeInfo(TypeInfo) -
Method in class escjava.vcGeneration.ProverType
TypeInfo represents a single translation/mapping between an old
type name and the targeted prover type name.
- getTypeInfo() -
Method in class escjava.vcGeneration.TNode
- Return the typeInfo associated with this node.
- getTypeInfo() -
Method in class escjava.vcGeneration.TypeInfo
-
- getTypeInfo(TypeInfo) -
Method in class escjava.vcGeneration.coq.CoqProver
-
- getTypeInfo(TypeInfo) -
Method in class escjava.vcGeneration.pvs.PvsProver
-
- getTypeInfo(TypeInfo) -
Method in class escjava.vcGeneration.sammy.SammyProver
-
- getTypeInfo(TypeInfo) -
Method in class escjava.vcGeneration.simplify.SimplifyProver
-
- getTypeInfo(TypeInfo) -
Method in class escjava.vcGeneration.xml.XmlProver
- Since our XML mapping of type names is the identity one, we may simply
return the old type name here.
- getTypeName() -
Method in class javafe.tc.TypeSig
- Return our exact type name, omitting the package name, as a
human-readable string suitable for display.
- getTypeOrNull(VarInit) -
Static method in class javafe.tc.FlowInsensitiveChecks
- Retrieves the
Type of a VarInit.
- getUniverse(ASTNode) -
Static method in class javafe.parser.ParseUtil
-
- getVariableInfo(VariableInfo) -
Method in class escjava.vcGeneration.ProverType
VariableInfo represents a single translation/mapping between an old
variable name and the targeted prover variable name.
- getVariableInfo(String) -
Static method in class escjava.vcGeneration.TNode
- return the
VariableInfo object associated with this name
- getVariableInfo() -
Method in class escjava.vcGeneration.TNode
- return the
VariableInfo object associated of the caller which
must be an instance of TName.
- getVariableInfo() -
Method in class escjava.vcGeneration.VariableInfo
-
- getVariableInfo(VariableInfo) -
Method in class escjava.vcGeneration.coq.CoqProver
- Returns a valid Coq name corresponding to the given VariableInfo.
- getVariableInfo(VariableInfo) -
Method in class escjava.vcGeneration.pvs.PvsProver
-
- getVariableInfo(VariableInfo) -
Method in class escjava.vcGeneration.sammy.SammyProver
-
- getVariableInfo(VariableInfo) -
Method in class escjava.vcGeneration.simplify.SimplifyProver
-
- getVariableInfo(VariableInfo) -
Method in class escjava.vcGeneration.xml.XmlProver
- Since our XML mapping of variable names is the identity one, we may simply
return the old variable name here.
- gets(VariableAccess, Expr) -
Static method in class escjava.translate.GC
-
- gf -
Variable in class escjava.gui.GUI.GFCUTreeValue
-
- globalStatus -
Static variable in class escjava.translate.NoWarn
-
- globallyTurnOffChecks(boolean) -
Static method in class escjava.translate.Translate
- If the flag is true, set all assertion checks to assumes.
- guard -
Variable in class escjava.ast.LoopCmd
-
- guard(Expr, Expr) -
Method in class escjava.translate.Translate
- Computes purity information for Java expression
e, translates
e (emitting any code needed to account for impurities or side
effects in the expression), and emits code that performs a RAISE
label command if the expression evaluates to false.
- guardVars -
Variable in class escjava.Options
-
- guardedVC -
Variable in class escjava.Options
-
- guardedVCDir -
Variable in class escjava.Options
-
- guardedVCFileExt -
Variable in class escjava.Options
-
- guardedVCFileNumbers -
Variable in class escjava.Options
-
- guardedVCGuardFile -
Variable in class escjava.Options
-
- guardedVCPrefix -
Variable in class escjava.Options
-
- guessPredicate(Expr, Expr, Type, ExprVec, int, Expr, ExprVec) -
Method in class escjava.pa.PredicateAbstraction
-
- gui -
Static variable in class escjava.gui.GUI
-
- guilight -
Variable in class escjava.gui.EscFrame
-
- guioptionPanel -
Variable in class escjava.gui.EscFrame
-
- guioptions -
Static variable in class escjava.gui.GuiOptionsPanel
-
CompilationUnit that
this tool processes.
CompilationUnit
that this tool processes.
Options
subclass.
IOException resulting from a read on SubProcess.from into a fatal error.
FlowInsensitiveChecks.inAnnotation is true.
Identifier for a given
sequence of characters.
this such that two
Names that are equals have the same hash
code.
this such that two
Names that are equals have the same
hash code.
this such that two
Names that are equals have the same hash
code.
s and prints an error message for the
houdini log to out.
ProverInterface#declare_axiom(Formula) and ProverInterface#make_assumption(Formula) calls.
Identifier is a symbol, that is, a sequence of
characters. Info class is responsible for displaying verbose
and debugging information to the user.
collectInvariants and its callers, *
extendSpecForCall and extendSpecForBody.loc, or to none if loc is the null location.
this.
this.
this.
expr or any of its subexpressions
mutates the heap or local variables.
n characters further
to the right of loc on the same line.
TypeReader
R for our underlying Java file space.
insideNoPats is really a parameter to *
printTerm.
instanceInitializers.
integralPrintName by symbolic
names.
Identifier associated with
s.
true when e is a boolean
literal expression whose value is b.
s is string that indicates
which ESC/Java check the program violates.
true only if e represents an
expression equivalent to false.
PRE.
LS is allowed in this context.
true if and only if r is a helper
routine that has not been visited by this FindContributor
object.
tag a PrimitiveType keyword?
\result is allowed in this context when isRESContext
is true and returnType !
- isRecursiveInvocation(RoutineDecl) -
Method in class escjava.translate.Translate
-
- isRedundant() -
Method in class escjava.ast.ExprDeclPragma
-
- isRedundant() -
Method in class escjava.ast.NamedExprDeclPragma
-
- isRedundant(int) -
Static method in class escjava.ast.TagConstants
-
- isRedundant() -
Method in class javafe.ast.ModifierPragma
-
- isRedundant() -
Method in class javafe.ast.StmtPragma
-
- isRedundant() -
Method in class javafe.ast.TypeDeclElemPragma
-
- isReferenceOrNullType(Type) -
Static method in class javafe.tc.Types
-
- isReferenceType(Type) -
Static method in class javafe.tc.Types
-
- isRoutineModifier(int) -
Static method in class escjava.AnnotationHandler.NestedPragmaParser
-
- isSameFormalParaDeclVec(FormalParaDeclVec, FormalParaDeclVec) -
Static method in class javafe.tc.Types
-
- isSameMethodSig(MethodDecl, MethodDecl) -
Static method in class javafe.tc.Types
-
- isSameType(Type, Type) -
Static method in class javafe.tc.Types
-
- isSameTypeInstance(Type, Type) -
Method in class escjava.tc.Types
-
- isSameTypeInstance(Type, Type) -
Method in class javafe.tc.Types
-
- isShortType(Type) -
Static method in class javafe.tc.Types
-
- isShowing() -
Method in class escjava.gui.EscFrame.EscTreeCellRenderer
-
- isSimple(Expr) -
Static method in class escjava.translate.GC
-
- isSimpleConjunction(Expr) -
Static method in class escjava.sp.SPVC
-
- isSimpleExpr(Expr) -
Static method in class escjava.sp.SPVC
-
- isSpecDesignatorContext -
Variable in class escjava.tc.FlowInsensitiveChecks
- Acts as a parameter to
checkExpr.
- isStandaloneConstructor(RoutineDecl) -
Method in class escjava.translate.Translate
-
- isStartOfUnaryExpressionNotPlusMinus(int) -
Method in class escjava.parser.EscPragmaParser
-
- isStartOfUnaryExpressionNotPlusMinus(int) -
Method in class javafe.parser.ParseExpr
- Determines whether the tag is the first token of a
UnaryExpressionNotPlusMinus.
- isStarted -
Static variable in class escjava.ProverManager
-
- isStatementExpression(Expr) -
Static method in class javafe.parser.ParseStmt
-
- isStatic(FieldDecl) -
Static method in class escjava.tc.GhostEnv
-
- isStatic -
Variable in class escjava.translate.InvariantInfo
-
- isStatic(int) -
Static method in class javafe.ast.Modifiers
-
- isStatic() -
Method in class javafe.tc.TypeSig
- Are we (possibly implicitly) static?
- isStaticContext() -
Method in class escjava.tc.EnvForGhostLocals
- Is there a current instance in scope?
- isStaticContext() -
Method in class javafe.tc.Env
- Is there a current instance in scope?
- isStaticContext() -
Method in class javafe.tc.EnvForCU
- Is there a current instance in scope?
- isStaticContext() -
Method in class javafe.tc.EnvForEnclosedScope
- Is there a current instance in scope?
- isStaticContext() -
Method in class javafe.tc.EnvForLocalType
- Is there a current instance in scope?
- isStaticContext() -
Method in class javafe.tc.EnvForLocals
- Is there a current instance in scope?
- isStaticContext() -
Method in class javafe.tc.EnvForTypeSig
- Is there a current instance in scope?
- isStaticMethod() -
Method in class escjava.ast.DerivedMethodDecl
-
- isStaticallyNonNull(VarInit) -
Static method in class escjava.backpred.BackPred
- Do we know statically that an expression always returns a
non-null value?
- isStrictFP(int) -
Static method in class javafe.ast.Modifiers
-
- isSubClassOrEq(Type, Type) -
Static method in class javafe.tc.Types
- Returns true iff
x is a superclass or
superinterface of y, or if x is the
same type as y.
- isSubclassOf(Type, TypeSig) -
Static method in class javafe.tc.Types
- Returns true if and only if
x is a subclass or
superinterface of y.
- isSubtypeOf(TypeSig) -
Method in class javafe.tc.TypeSig
-
- isSynchronized() -
Method in class escjava.ast.DerivedMethodDecl
-
- isSynchronized(int) -
Static method in class javafe.ast.Modifiers
-
- isTopLevelType() -
Method in class javafe.tc.TypeSig
- Are we a top-level type?
- isTraceLabel(String) -
Static method in class escjava.translate.ErrorMsg
- Returns whether or not
s is string that indicates
information about the execution trace in the counterexample
context.
- isTrue(Expr) -
Static method in class escjava.AnnotationHandler
- Returns true if the argument is literally true, and returns false if it is
not a literal or is literally false.
- isTrue(ASTNode) -
Method in class escjava.ast.Utils.BooleanDecoration
-
- isTrueLiteral(Expr) -
Method in class escjava.translate.Frame
- A utility function that returns true if the argument
expression is null or strictly equal to a boolean TRUE.
- isTwoStateContext -
Variable in class escjava.tc.FlowInsensitiveChecks
- Indicates whether
\old and \fresh are allowed in
this context.
- isTypeType(Type) -
Static method in class escjava.tc.Types
-
- isValidTag(int) -
Static method in class escjava.ast.EscPrimitiveType
-
- isValidTag() -
Method in class escjava.ast.EscPrimitiveType
-
- isValidTag(int) -
Static method in class javafe.ast.JavafePrimitiveType
-
- isValidTag() -
Method in class javafe.ast.JavafePrimitiveType
-
- isValidTag(int) -
Static method in class javafe.ast.LiteralExpr
-
- isValidTag() -
Method in class javafe.ast.PrimitiveType
-
- isValidValue(int, Object) -
Static method in class javafe.ast.LiteralExpr
-
- isVariable(Expr) -
Static method in class javafe.tc.FlowInsensitiveChecks
-
- isVoidType(Type) -
Static method in class javafe.tc.Types
-
- isVolatile(int) -
Static method in class javafe.ast.Modifiers
-
- isWholeFile -
Variable in class javafe.util.LocationManagerCorrelatedReader
- Are all of our locations whole-file locations?
- isWholeFileLoc(int) -
Static method in class javafe.util.Location
- Check if a location is a whole file location.
- isWholeFileLoc(int) -
Static method in class javafe.util.LocationManagerCorrelatedReader
- Is a location a whole file location?
- isWideningPrimitiveConvertable(Type, Type) -
Static method in class javafe.tc.Types
-
- isWideningPrimitiveConvertableInstance(Type, Type) -
Method in class escjava.tc.Types
-
- isWideningPrimitiveConvertableInstance(Type, Type) -
Method in class javafe.tc.Types
-
- isWideningReferenceConvertable(Type, Type) -
Static method in class javafe.tc.Types
-
- isWideningReferenceConvertableInstance(Type, Type) -
Method in class javafe.tc.Types
-
- isZipFilename(String) -
Static method in class javafe.filespace.PathComponent
- Does a filename indicate that it is in zip format?
- is_valid(Formula, Properties) -
Method in class escjava.prover.Cvc3
- Perform a query on a formula.
- is_valid(Formula, Properties) -
Method in class escjava.prover.Harvey
-
- is_valid(Formula, Properties) -
Method in class escjava.prover.NewProver
- Check the validity of the given formula given the current theory,
its axioms, and the current set of assumptions.
- is_valid(Formula, Properties) -
Method in class escjava.prover.Sammy
-
- isroot -
Variable in class escjava.vcGeneration.TNode
-
- issueCautions -
Variable in class escjava.translate.Frame
- The value of issueCautions obtained from the Translate owner
- issueCautions -
Variable in class escjava.translate.Translate
- Indicates whether to issue cautions.
- issueUsage -
Variable in class javafe.Options
- True if we should simply issue a usage message and abort.
- items -
Variable in class escjava.ast.ModifiesGroupPragma
-
FilterCorrelatedReader creates the illusion that the
additional \@-signs, etc. allowed in the JML annotation syntax are
really just whitespace.JmlCorrelatedReader with
child as the underlying CorrelatedReader.
Query engine for determining the GenericFiles for files that belong to Java packages.
CorrelatedReader.
CorrelatedReader.
CompilationUnit-loading
notification events (sent by OutsideEnv). CorrelatedReader class manages the allocation of
location numbers.Enumeration in
terms of a single function that returns the next element in a
series, or null if the series is exhausted.Listener to notify when a CompilationUnit
is loaded.
CompilationUnits we have loaded
so far.
this.
this.
this.
this.
this.
this.
loc.
loc.
loc.
loc.
loc.
loc.
GenericFile
representing that file.
P.T, then return a GenericFile representing
that file.
TypeSig for fully-qualified
package-member name P.T.
lookup except that checking the existence of
the type is deferred until it's TypeDecl is touched
for the first time.
getNextToken reads ahead one character
and leaves the result in m_nextchr.
args.
args.
args.
args.
lookup on a series of package-member-type
names.
EscTypeReader from a query engine, a
source reader, and a binary reader.
EscTypeReader from a non-null query
engine and a pragma parser.
EscTypeReader using a given Java
classpath for our underlying Java file space and a given pragma
parser.
EscTypeReader using a the default Java
classpath for our underlying Java file space and a given pragma
parser.
EscTypeReader using the default Java
classpath for our underlying Java file space and no pragma
parser.
Name with the given identifiers and
locations.
Name whose locations are all
loc from a String.
StandardTypeReader from a query engine, a
source reader, and a binary reader.
StandardTypeReader from a query engine and
a pragma parser.
StandardTypeReader using a given Java
classpath for our underlying Java file space and a given pragma
parser.
StandardTypeReader using a the default Java
classpath for our underlying Java file space and a given pragma
parser.
StandardTypeReader using the default Java
classpath for our underlying Java file space and no pragma
parser.
GhostEnv instead of EnvForTypeSig.
expr is
impure.
code commands that make up a loop with nominal body
guard;body, where label is raised within
body to terminate the loop.
Options object.
PrettyPrint.inst to.
PrettyPrint.inst to.
StandardTypeReader to be used for
locating and reading in types.
TypeCheck
class (or a subclass thereof) to be used for typechecking.
Strings to already created
non-null Atoms.
merge method below.
TypeDecl associated with this,
including inherited ones.
parseModifiers mutates this
value.
readCheck and writeCheck to accumulate the
list of mutexes protecting a shared variable.
File)
as a GenericFile.File.
Assert to signal that an
unimplemented feature has been encountered. post all NonNullInit checks for non_null instance
fields and instance ghost fields declared in td.
GenericVarDecl's to point to * NonNullPragmas
(SimpleModifierPragma's).
gc.
CompilationUnit to loaded.
CompilationUnit is loaded by
OutsideEnv, this routine in the current
Listener (see OutsideEnv.setListener)
is called with the newly-loaded
CompilationUnit.
loc that guarded command expression
e, which was translated from the Java expression E,
is not null.
OperatorTags is a class defining a partially-opaque
type for tags used in the AST. OutsideEnv implements the top-level environment
consisting of only the package-member types.
loc on a given line number in a given stream?
PathComponent)
specified by a classpath.
count number to the
given label expression's label name, so that trace labels will sort correctly.
on is
set.
out in the superclass).
Simplify.readySubProcess() is called first.
null if we are closed.
collectParamsAndGlobalVars and its *
caller, extendSpecForCall.Parse objects parse Java statements, creating AST
structures for the parsed input using the static
make*() methods of the classes in the
javafe.ast package.
Tree
(cf PathComponent) where some files and directories that
are clearly not part of the Java namespace have been filtered out;
the remaining nodes can be divided into two categories: (a)
(usually interior) nodes that correspond to potential Java
packages, and (b) exterior nodes that correspond to files that
reside in one of the potential Java packages and that have an
extension (e.g., .java).PragmaParser objects are called by Lex
objects to parse pragmas out of pragma-containing comments. PrintSpec print specs for class files.Block.
ConstructorBody.
exsures or
signals pragma.
exsures or
signals pragma.
exsures or
signals pragma parameter.
exsures or
signals pragma parameter.
exsures or
signals pragma.
Identifier.
ModifierPragmaVec.
Name.
l.
l,
given the prefix primary expression primary.
PrimitiveType.
l.
Stmt.
suffix, which is expected to have one of the forms
Number "."
Type, either a primitive type, a type name, or
an array type.
TypeName.
typeDecl.
SubProcess.getChar(), but leaves the character in the stream.
TypeDeclElems
inside the this.
TypeDeclElemss
inside the this.
handleCU has been
called on each CompilationUnit to process them.
handleCU has been called
on each CompilationUnit to process them.
Name consisting of the first
len identifiers of this.
Name consisting of the first
len identifiers of this.
this to the "prepped" state.
handleCU is called
on each CompilationUnit to process them.
handleCU is called
on each CompilationUnit to process them.
PrintStream.
PrintStream.
PrintStream.
PrintStream.
PrintStream.
PrintStream.
System.out.
PrintStream.
PrintStream.
name,
where labelList and
counterexampleContext are labels and
counterexample from Simplify.
s and prints a nice error message to
out.
Type as a
String.
Types as a String
containing a parenthesized list of user-readable names.
s and prints execution trace information to
out.
Vector is
aliased with a variable in SrcTool.
args.
exp.
expr nor any of its
subexpressions mutate the heap or local variables.
o.
Query for use in creating a
StandardTypeReader from a Java classpath.
GenericFile,
returning a CompilationUnit. EC= label; raise to code.
StandardTypeReader.read(String[], String, boolean)
method to include ".spec" files.
CompilationUnit from
CompilationUnit from either
the binaries for P.T if they are up to date, or from
the source for P.T.
CorrelatedReader class.
CorrelatedReader class.
null, this buffer keeps a record of (some
of) the characters read from this subprocess using SubProcess.getChar().
pending.
SLists from this
subprocess.
CompilationUnit from the binaries for the fully-qualified
outside type P.T.
CompilationUnit from the
source for the fully-qualified outside type P.T.
stops, or an EOF.
TypeReader for our underlying Java file space.
mark method was last called on this input stream.
mark method was last called on this input stream.
computeTypeSpecific.
this to the supertype links resolved
state.
CorrelatedReader.
map restricted to the
domain e.
TProofTyperVisitor.
args are the
command-line arguments we have been invoked with.
SInt representing a given
int.
SLists represent possibly-empty lists of
SExps.
SList may not be extended outside this package.
SNil instance represents the empty list of
SExps.SPair is a pair of a SExp and a
SList; together with the SNil class, it is
used to implement lists of SExps. Reader that reads in a CompilationUnit from a source file (.java files) using the
javafe.parser package.
SrcTool is an abstract class for tools that use
our Java front end to process the CompilationUnits
found in source files. TypeReader that uses SlowQuery to find type files, and user-supplied
Readers to read source and binary files.StandardTypeReader from a query engine, a
source reader, and a binary reader.
match.
Token fields of this along the way.
to from from.
String command to Simplify.
String containing zero-or-more commands to
our Simplify subprocess.
0 < cmds.size().
cmds.
ParseStmt
functions.
ASTNode.
java.class.path.
ith element to
s.
init with d; will be returned by a call
to getInitVar.
Listener to be notified about
CompilationUnit loading.
cu.
XmlProver.stylesheet to be set once.
id.
System.err.
System.err.
System.err.
TypeDecl nodes to point to
TypeSig objects.
SimpleTargets[[ gc ]] (as defined in ESCJ 16)
to set.
null if it
has not yet been allocated.
this.
this.
this.
n.
n (see above),
except returns -1 if the size exceeds limit.
check; checks for duplicates.
PrintStream.
TrSpecExpr
described in ESCJ 16.
this.
id,
where id has previously been returned by
toStreamId.
id, where id has previously been
returned by locToStreamId.
XmlProver.getProof(java.io.Writer, java.lang.String, escjava.vcGeneration.TNode)
CECEnum that is currently using
Simplify (there can be at most 1 such CECEnum), or
null if there is no such CECEnum.
suffix.
suffix, if any,
and the null location if suffix is not a valid suffix.
assume for each
precondition in spec, then does body, then
checks the postconditions of spec, and finally checks the
modifies constraints implied by spec.
Boolean
value and variables from usual Prop.
Boolean
value and variables from usual Prop.
TagConstants is a class defining a partially-opaque
type for tags used in the AST. TagConstants is a class defining the constants used to
identify different kinds of tokens.- TagConstants() -
Constructor for class javafe.parser.TagConstants
-
- TagConstants - class javafe.tc.TagConstants.
-
- TagConstants() -
Constructor for class javafe.tc.TagConstants
-
- Targets - class escjava.translate.Targets.
- Provides methods for computing various kinds of syntactic targets
- Targets() -
Constructor for class escjava.translate.Targets
-
- TaskQueue - class escjava.gui.TaskQueue.
-
- TaskQueue() -
Constructor for class escjava.gui.TaskQueue
-
- TeeOutputStream - class escjava.prover.TeeOutputStream.
- This class is a
FilterOutputStream class that forwards its
given output to two given OutputStreams. - TeeOutputStream(OutputStream, OutputStream) -
Constructor for class escjava.prover.TeeOutputStream
- Creates an output stream filter built on top of two specified
underlying output streams.
- TestCase - class junitutils.TestCase.
- Some utility methods for test cases
- TestCase(String) -
Constructor for class junitutils.TestCase
-
- TestFilesTestSuite - class junitutils.TestFilesTestSuite.
- This is a JUnit TestSuite that is created from a number of tests as follows.
- TestFilesTestSuite() -
Constructor for class junitutils.TestFilesTestSuite
-
- TestFilesTestSuite(String, String, String[], Class) -
Constructor for class junitutils.TestFilesTestSuite
- A constructor for this test suite.
- TestFilesTestSuite.Helper - class junitutils.TestFilesTestSuite.Helper.
- This is a helper class that is actually a TestCase; it is run repeatedly
with different constructor arguments.
- TestFilesTestSuite.Helper(String, String[]) -
Constructor for class junitutils.TestFilesTestSuite.Helper
- The first argument is used as the name of the test as well as
the name of the file to be tested.
- TestTool - class javafe.TestTool.
TestTool is an test class for SrcTool and
its superclasses. - TestTool() -
Constructor for class javafe.TestTool
-
- TestTool.Options - class javafe.TestTool.Options.
-
- TestTool.Options() -
Constructor for class javafe.TestTool.Options
-
- ThisExpr - class javafe.ast.ThisExpr.
- We represent [C.]this.
- ThisExpr(Type, int) -
Constructor for class javafe.ast.ThisExpr
-
- ThrowStmt - class javafe.ast.ThrowStmt.
-
- ThrowStmt(Expr, int) -
Constructor for class javafe.ast.ThrowStmt
-
- ToStream() -
Method in class escjava.prover.SubProcess
-
- Token - class javafe.parser.Token.
- The
Token class defines a set of fields that describe
lexical tokens.
- Token() -
Constructor for class javafe.parser.Token
- *
Creation: *
*
- TokenQueue - class javafe.parser.TokenQueue.
-
- TokenQueue() -
Constructor for class javafe.parser.TokenQueue
-
- Tool - class javafe.Tool.
Tool is an abstract class for tools.
- Tool() -
Constructor for class javafe.Tool
-
- TrAnExpr - class escjava.translate.TrAnExpr.
- Translates Annotation Expressions to GCExpr.
- TrAnExpr() -
Constructor for class escjava.translate.TrAnExpr
-
- Translate - class escjava.translate.Translate.
-
- Translate() -
Constructor for class escjava.translate.Translate
-
- Translate.EverythingLoc - class escjava.translate.Translate.EverythingLoc.
-
- Translate.EverythingLoc(int, Hashtable) -
Constructor for class escjava.translate.Translate.EverythingLoc
-
- Translate.Strings - class escjava.translate.Translate.Strings.
-
- Translate.Strings() -
Constructor for class escjava.translate.Translate.Strings
-
- Traverse - class escjava.pa.Traverse.
-
- Traverse() -
Constructor for class escjava.pa.Traverse
-
- Tree - class javafe.filespace.Tree.
- A Tree is a n-ary tree with data at each node; the direct children of a
node are unordered but distinguished via String labels on the edges
to them.
- Tree(Object) -
Constructor for class javafe.filespace.Tree
- Create a root node:
- Tree(Tree, String, Object) -
Constructor for class javafe.filespace.Tree
- Create a non-root node:
- TreeWalker - class javafe.filespace.TreeWalker.
- This class provides a way to enumerate all the nodes of a
given Tree in depth-first pre-order using lexical ordering on
siblings.
- TreeWalker(Tree) -
Constructor for class javafe.filespace.TreeWalker
- From a Tree create an enumeration that enumerates
all of the Tree's nodes (including the root node first).
- TreeWalker_ArrayEnum - class javafe.filespace.TreeWalker_ArrayEnum.
- A Enumeration for enumerating the members of an array of Objects.
- TreeWalker_ArrayEnum(Object[]) -
Constructor for class javafe.filespace.TreeWalker_ArrayEnum
-
- TriggerlessQuantWarning - class escjava.prover.TriggerlessQuantWarning.
- An object of this class represent a "result" produced by Simplify.
- TriggerlessQuantWarning(SList, SList, SExp, int, SExp) -
Constructor for class escjava.prover.TriggerlessQuantWarning
-
- TryCatchStmt - class javafe.ast.TryCatchStmt.
- Represents a try-catch statement.
- TryCatchStmt(Stmt, CatchClauseVec, int) -
Constructor for class javafe.ast.TryCatchStmt
-
- TryFinallyStmt - class javafe.ast.TryFinallyStmt.
-
- TryFinallyStmt(Stmt, Stmt, int, int) -
Constructor for class javafe.ast.TryFinallyStmt
-
- Type - class javafe.ast.Type.
- Represents a Type syntactic unit.
- Type() -
Constructor for class javafe.ast.Type
-
- Type(TypeModifierPragmaVec) -
Constructor for class javafe.ast.Type
-
- TypeCheck - class escjava.tc.TypeCheck.
-
- TypeCheck() -
Constructor for class escjava.tc.TypeCheck
- Creates a singleton instance of this class, and sets the
inst
field to this instance.
- TypeCheck - class javafe.tc.TypeCheck.
- The
TypeCheck class contains methods to disambiguate, resolve,
and check type declarations. - TypeCheck() -
Constructor for class javafe.tc.TypeCheck
- Creates a instance of TypeCheck, and sets the
inst
field to this instance.
- TypeDecl - class javafe.ast.TypeDecl.
- Represents a TypeDeclaration.
- TypeDecl(int, ModifierPragmaVec, Identifier, TypeNameVec, TypeModifierPragmaVec, TypeDeclElemVec, int, int, int, int) -
Constructor for class javafe.ast.TypeDecl
-
- TypeDeclElem - interface javafe.ast.TypeDeclElem.
- Represents either a ClassBodyDeclaration or an
InterfaceMemberDeclaration.
- TypeDeclElemPragma - class javafe.ast.TypeDeclElemPragma.
-
- TypeDeclElemPragma() -
Constructor for class javafe.ast.TypeDeclElemPragma
-
- TypeDeclElemPragma(boolean) -
Constructor for class javafe.ast.TypeDeclElemPragma
-
- TypeDeclElemVec - class javafe.ast.TypeDeclElemVec.
-
- TypeDeclElemVec(TypeDeclElem[]) -
Constructor for class javafe.ast.TypeDeclElemVec
- *
Private constructors: *
*
- TypeDeclElemVec(int) -
Constructor for class javafe.ast.TypeDeclElemVec
-
- TypeDeclVec - class javafe.ast.TypeDeclVec.
-
- TypeDeclVec(TypeDecl[]) -
Constructor for class javafe.ast.TypeDeclVec
- *
Private constructors: *
*
- TypeDeclVec(int) -
Constructor for class javafe.ast.TypeDeclVec
-
- TypeExpr - class escjava.ast.TypeExpr.
-
- TypeExpr(int, int, Type) -
Constructor for class escjava.ast.TypeExpr
-
- TypeInfo - class escjava.vcGeneration.TypeInfo.
-
- TypeInfo(String) -
Constructor for class escjava.vcGeneration.TypeInfo
-
- TypeInfo(String, String, ProverType) -
Constructor for class escjava.vcGeneration.TypeInfo
- Constructor for specifying the renaming of the type.
- TypeModifierPragma - class javafe.ast.TypeModifierPragma.
-
- TypeModifierPragma() -
Constructor for class javafe.ast.TypeModifierPragma
-
- TypeModifierPragmaVec - class javafe.ast.TypeModifierPragmaVec.
-
- TypeModifierPragmaVec(TypeModifierPragma[]) -
Constructor for class javafe.ast.TypeModifierPragmaVec
- *
Private constructors: *
*
- TypeModifierPragmaVec(int) -
Constructor for class javafe.ast.TypeModifierPragmaVec
-
- TypeName - class javafe.ast.TypeName.
-
- TypeName(TypeModifierPragmaVec, Name) -
Constructor for class javafe.ast.TypeName
-
- TypeNameVec - class javafe.ast.TypeNameVec.
-
- TypeNameVec(TypeName[]) -
Constructor for class javafe.ast.TypeNameVec
- *
Private constructors: *
*
- TypeNameVec(int) -
Constructor for class javafe.ast.TypeNameVec
-
- TypeObjectDesignator - class javafe.ast.TypeObjectDesignator.
- Represents a ObjectDesignator of the form "TypeName . "
Is created from AmbiguousVariableAccess/AmbiguousMethodInvocation
by the name resolution code.
- TypeObjectDesignator(int, Type) -
Constructor for class javafe.ast.TypeObjectDesignator
-
- TypePrint - class javafe.tc.TypePrint.
-
- TypePrint() -
Constructor for class javafe.tc.TypePrint
-
- TypePrint(PrettyPrint, PrettyPrint) -
Constructor for class javafe.tc.TypePrint
-
- TypeReader - class javafe.reader.TypeReader.
- A TypeReader is an extended
Reader that understands how to
read in Java reference types given either a fully-qualified name or
a source file (in the form of a GenericFile). - TypeReader() -
Constructor for class javafe.reader.TypeReader
-
- TypeSig - class escjava.tc.TypeSig.
-
- TypeSig(String[], String, TypeSig, TypeDecl, CompilationUnit) -
Constructor for class escjava.tc.TypeSig
-
- TypeSig(String, Env, TypeDecl) -
Constructor for class escjava.tc.TypeSig
-
- TypeSig - class javafe.tc.TypeSig.
- A
TypeSig is a proxy and adaptor for TypeDecl. - TypeSig(String, Env, TypeDecl) -
Constructor for class javafe.tc.TypeSig
- Create a TypeSig that represents a non-member type.
- TypeSig(String[], String, TypeSig, TypeDecl, CompilationUnit) -
Constructor for class javafe.tc.TypeSig
- Create a TypeSig that represents a member type.
- TypeSig(String[], String, TypeDecl, CompilationUnit) -
Constructor for class javafe.tc.TypeSig
- Create a TypeSig that represents an internal-use-only
package-member type.
- TypeSigVec - class javafe.tc.TypeSigVec.
-
- TypeSigVec(TypeSig[]) -
Constructor for class javafe.tc.TypeSigVec
- *
Private constructors: *
*
- TypeSigVec(int) -
Constructor for class javafe.tc.TypeSigVec
-
- Types - class escjava.tc.Types.
-
- Types() -
Constructor for class escjava.tc.Types
-
- Types - class javafe.tc.Types.
-
- Types() -
Constructor for class javafe.tc.Types
-
- table -
Variable in class escjava.sp.VarMap
-
- tag -
Variable in class escjava.ast.CondExprModifierPragma
-
- tag -
Variable in class escjava.ast.DependsPragma
-
- tag -
Variable in class escjava.ast.ExprDeclPragma
-
- tag -
Variable in class escjava.ast.ExprModifierPragma
-
- tag -
Variable in class escjava.ast.ExprStmtPragma
-
- tag -
Variable in class escjava.ast.IdExprDeclPragma
-
- tag -
Variable in class escjava.ast.IdentifierModifierPragma
-
- tag -
Variable in class escjava.ast.MapsExprModifierPragma
-
- tag -
Variable in class escjava.ast.ModelProgamModifierPragma
-
- tag -
Variable in class escjava.ast.ModifiesGroupPragma
-
- tag -
Variable in class escjava.ast.NamedExprDeclPragma
-
- tag -
Variable in class escjava.ast.SimpleModifierPragma
-
- tag -
Variable in class escjava.ast.SimpleStmtPragma
-
- tag -
Variable in class escjava.ast.VarDeclModifierPragma
-
- tag -
Variable in class escjava.ast.VarExprModifierPragma
-
- tag -
Variable in class javafe.ast.LiteralExpr
-
- tag -
Variable in class javafe.ast.PrimitiveType
-
- tags -
Static variable in class javafe.ast.TagConstants
-
- tail -
Variable in class escjava.prover.SPair
- The tail of our list; this field should not be modified by
clients and should be non-null.
- target -
Variable in class escjava.ast.DependsPragma
-
- target -
Variable in class escjava.ast.NamedExprDeclPragma
-
- target -
Variable in class escjava.ast.SetStmtPragma
-
- target -
Variable in class escjava.ast.SubstExpr
-
- targetExtension -
Variable in class javafe.filespace.PkgTree_MatchesExtension
-
- targetTypeCorrect(GenericVarDecl, Hashtable) -
Static method in class escjava.translate.TrAnExpr
- This method implements the ESCJ 16 function
TargetTypeCorrect,
except for the init$ case!
- targets -
Variable in class escjava.ast.Spec
-
- targets -
Static variable in class escjava.translate.ATarget
-
- tasks -
Variable in class escjava.gui.TaskQueue
-
- tasks -
Static variable in class escjava.gui.WindowTasks
-
- td -
Variable in class escjava.AnnotationHandler
-
- td -
Variable in class escjava.gui.GUI.TDTreeValue
-
- td -
Variable in class escjava.translate.Frame.ModifiesIterator
- The TypeDecl whose view of any datagroups is to be used.
- td -
Variable in class escjava.translate.RepHelper
-
- temp -
Static variable in class escjava.gui.EscOptions.MListener
-
- tempName(int, String, Type) -
Static method in class escjava.translate.TrAnExpr
-
- tempVars -
Variable in class escjava.ast.LoopCmd
-
- tempn -
Static variable in class escjava.translate.TrAnExpr
-
- temporaries -
Variable in class escjava.pa.PredicateAbstraction
-
- temporaries -
Variable in class escjava.translate.Translate
- Contains the temporaries that generated for the current method that haven't
yet been declared in a VARINCMD.
- temporary(String, int) -
Method in class escjava.translate.Translate
- Generate a temporary variable with prefix
s and associated
expression location information locAccess.
- temporary(String, int, int) -
Method in class escjava.translate.Translate
-
- temporaryVariable -
Static variable in class escjava.translate.UniqName
- Use this location *only* in declarations of temporary variables
(see case 6 of ESCJ 23b for rules on the names allowed for these).
- term(String, String, TFunction) -
Method in class escjava.vcGeneration.xml.TXmlVisitor
-
- termNumber -
Static variable in class escjava.translate.VcToString
-
- test -
Variable in class javafe.ast.CondExpr
-
- test -
Variable in class javafe.ast.ForStmt
-
- testMode -
Variable in class javafe.Options
- When true, no variable output (e.g., execution time) is
printed, so that output can be compared to an oracle output
file.
- testName -
Variable in class junitutils.TestFilesTestSuite
- The name of this test suite.
- testRef -
Variable in class escjava.Options
- When true, pretty prints each compilation unit on the command-line;
this is only used for testing, to test the combining of refinements.
- text -
Variable in class javafe.parser.Lex
- The characters that constitute the current token.
- textArea -
Variable in class escjava.gui.EscOutputFrame
-
- textlen -
Variable in class javafe.parser.Lex
- The number of characters in the current token.
- theMark -
Static variable in class escjava.translate.LabelInfoToString
-
- thisId -
Static variable in class escjava.translate.Frame
- A precomputed Identifier for 'this', to be used in constructing
Expressions.
- this_class_index -
Variable in class javafe.reader.ASTClassFileParser
- The contant pool index of this class.
- thisexpr -
Static variable in class escjava.translate.Substitute
-
- thisvar -
Static variable in class escjava.translate.GC
-
- thn -
Variable in class javafe.ast.CondExpr
-
- thn -
Variable in class javafe.ast.IfStmt
-
- throwsSet -
Variable in class escjava.ast.DerivedMethodDecl
-
- timeUsed(long) -
Static method in class javafe.Tool
- Compute the time used from a start time to now, then return it in
a user readable form.
- title -
Variable in class escjava.gui.WindowThread.HtmlTask
-
- tmodifiers -
Variable in class javafe.ast.AmbiguousMethodInvocation
-
- tmodifiers -
Variable in class javafe.ast.MethodInvocation
-
- tmodifiers -
Variable in class javafe.ast.RoutineDecl
-
- tmodifiers -
Variable in class javafe.ast.Type
- Does this AST Node have associated locations?
- tmodifiers -
Variable in class javafe.ast.TypeDecl
-
- tmpcount -
Variable in class escjava.translate.Translate
- Countains the number of temporaries generated for the method currently being
translated.
- to -
Variable in class escjava.prover.SubProcess
- The
PrintStream to the actual subprocess, or
null if we are closed.
- toArray() -
Method in class escjava.ast.CondExprModifierPragmaVec
-
- toArray() -
Method in class escjava.ast.ConditionVec
-
- toArray() -
Method in class escjava.ast.DecreasesInfoVec
-
- toArray() -
Method in class escjava.ast.DefPredVec
-
- toArray() -
Method in class escjava.ast.ExprDeclPragmaVec
-
- toArray() -
Method in class escjava.ast.ExprModifierPragmaVec
-
- toArray() -
Method in class escjava.ast.ExprStmtPragmaVec
-
- toArray() -
Method in class escjava.ast.GenericVarDeclVec
-
- toArray() -
Method in class escjava.ast.GuardedCmdVec
-
- toArray() -
Method in class escjava.ast.LocalVarDeclVec
-
- toArray() -
Method in class escjava.ast.ModifiesGroupPragmaVec
-
- toArray() -
Method in class escjava.ast.VarExprModifierPragmaVec
-
- toArray() -
Method in class javafe.ast.CatchClauseVec
-
- toArray() -
Method in class javafe.ast.ExprVec
-
- toArray() -
Method in class javafe.ast.FieldDeclVec
-
- toArray() -
Method in class javafe.ast.FormalParaDeclVec
-
- toArray() -
Method in class javafe.ast.IdentifierVec
-
- toArray() -
Method in class javafe.ast.ImportDeclVec
-
- toArray() -
Method in class javafe.ast.LexicalPragmaVec
-
- toArray() -
Method in class javafe.ast.MethodDeclVec
-
- toArray() -
Method in class javafe.ast.ModifierPragmaVec
-
- toArray() -
Method in class javafe.ast.StmtVec
-
- toArray() -
Method in class javafe.ast.TypeDeclElemVec
-
- toArray() -
Method in class javafe.ast.TypeDeclVec
-
- toArray() -
Method in class javafe.ast.TypeModifierPragmaVec
-
- toArray() -
Method in class javafe.ast.TypeNameVec
-
- toArray() -
Method in class javafe.ast.VarInitVec
-
- toArray() -
Method in class javafe.tc.TypeSigVec
-
- toCanonicalString(int, Object) -
Static method in class javafe.ast.PrettyPrint
- Returns a canonical text representation for literal values.
- toCanonicalString(int, Object) -
Static method in class javafe.ast.StandardPrettyPrint
- Requires that
tag is one of constants on the left of this
table:
TagConstants.BOOLEANLIT Boolean
TagConstants.CHARLIT Integer
TagConstants.DOUBLELIT Double
TagConstants.FLOATLIT Float
TagConstants.INTLIT Integer
TagConstants.LONGLIT Long
TagConstants.STRINGLIT String
and that val is an instance of the corresponding type
on the right.
- toClassTypeSig(Type) -
Static method in class javafe.tc.Types
- Returns the TypeSig for a Type x, if x denotes a class type,
otherwise returns null.
- toColor(int) -
Static method in class escjava.Status
-
- toColumn(int) -
Static method in class javafe.util.Location
- Extracts the column corresponding to a location.
- toDot() -
Method in class escjava.vcGeneration.VcGenerator
-
- toFile(int) -
Static method in class javafe.util.Location
- Extracts the file corresponding to a location.
- toFileLineString(int) -
Static method in class javafe.util.Location
-
- toFileName(int) -
Static method in class javafe.util.Location
- Extracts the filename corresponding to a location.
- toLineNumber(int) -
Static method in class javafe.util.Location
- Extracts the line number corresponding to a location.
- toNoWarnTag(String) -
Static method in class escjava.translate.NoWarn
- Convert a nowarn category to its tag.
- toNumber(String, int) -
Static method in class escjava.translate.ErrorMsg
- Converts the substring beginning at
k of s
into a number.
- toOffset(int) -
Static method in class javafe.util.Location
- Extracts the offset corresponding to a location.
- toStreamId(int) -
Static method in class javafe.util.Location
- Returns the internal stream ID used for the stream associated
with location
loc.
- toString(int) -
Static method in class escjava.Status
-
- toString() -
Method in class escjava.ast.AnOverview
- Return a string representation of
this.
- toString() -
Method in class escjava.ast.ArrayRangeRefExpr
-
- toString() -
Method in class escjava.ast.Call
-
- toString() -
Method in class escjava.ast.CmdCmdCmd
-
- toString() -
Method in class escjava.ast.CondExprModifierPragma
-
- toString() -
Method in class escjava.ast.CondExprModifierPragmaVec
-
- toString() -
Method in class escjava.ast.Condition
-
- toString() -
Method in class escjava.ast.ConditionVec
-
- toString() -
Method in class escjava.ast.DecreasesInfo
-
- toString() -
Method in class escjava.ast.DecreasesInfoVec
-
- toString() -
Method in class escjava.ast.DefPred
-
- toString() -
Method in class escjava.ast.DefPredApplExpr
-
- toString() -
Method in class escjava.ast.DefPredLetExpr
-
- toString() -
Method in class escjava.ast.DefPredVec
-
- toString() -
Method in class escjava.ast.DependsPragma
-
- toString() -
Method in class escjava.ast.DynInstCmd
-
- toString(int) -
Method in class escjava.ast.EscPrettyPrint
-
- toString() -
Method in class escjava.ast.EscPrimitiveType
-
- toString() -
Method in class escjava.ast.EverythingExpr
-
- toString() -
Method in class escjava.ast.ExprCmd
-
- toString() -
Method in class escjava.ast.ExprDeclPragma
-
- toString() -
Method in class escjava.ast.ExprDeclPragmaVec
-
- toString() -
Method in class escjava.ast.ExprModifierPragma
-
- toString() -
Method in class escjava.ast.ExprModifierPragmaVec
-
- toString() -
Method in class escjava.ast.ExprStmtPragma
-
- toString() -
Method in class escjava.ast.ExprStmtPragmaVec
-
- toString() -
Method in class escjava.ast.GCExpr
- Return a string representation of
this.
- toString() -
Method in class escjava.ast.GeneralizedQuantifiedExpr
-
- toString(int) -
Static method in class escjava.ast.GeneratedTags
-
- toString() -
Method in class escjava.ast.GenericVarDeclVec
-
- toString() -
Method in class escjava.ast.GetsCmd
-
- toString() -
Method in class escjava.ast.GhostDeclPragma
-
- toString() -
Method in class escjava.ast.GuardExpr
-
- toString() -
Method in class escjava.ast.GuardedCmd
- Return a string representation of
this.
- toString() -
Method in class escjava.ast.GuardedCmdVec
-
- toString() -
Method in class escjava.ast.IdExprDeclPragma
-
- toString() -
Method in class escjava.ast.IdentifierModifierPragma
-
- toString() -
Method in class escjava.ast.ImportPragma
-
- toString() -
Method in class escjava.ast.LabelExpr
-
- toString() -
Method in class escjava.ast.LocalVarDeclVec
-
- toString() -
Method in class escjava.ast.LockSetExpr
-
- toString() -
Method in class escjava.ast.LoopCmd
-
- toString() -
Method in class escjava.ast.MapsExprModifierPragma
-
- toString() -
Method in class escjava.ast.ModelConstructorDeclPragma
-
- toString() -
Method in class escjava.ast.ModelDeclPragma
-
- toString() -
Method in class escjava.ast.ModelMethodDeclPragma
-
- toString() -
Method in class escjava.ast.ModelProgamModifierPragma
-
- toString() -
Method in class escjava.ast.ModelTypePragma
-
- toString(int) -
Static method in class escjava.ast.Modifiers
-
- toString() -
Method in class escjava.ast.ModifiesGroupPragma
-
- toString() -
Method in class escjava.ast.ModifiesGroupPragmaVec
-
- toString() -
Method in class escjava.ast.NamedExprDeclPragma
-
- toString() -
Method in class escjava.ast.NaryExpr
-
- toString() -
Method in class escjava.ast.NestedModifierPragma
-
- toString() -
Method in class escjava.ast.NotModifiedExpr
-
- toString() -
Method in class escjava.ast.NotSpecifiedExpr
-
- toString() -
Method in class escjava.ast.NothingExpr
-
- toString() -
Method in class escjava.ast.NowarnPragma
-
- toString() -
Method in class escjava.ast.NumericalQuantifiedExpr
-
- toString() -
Method in class escjava.ast.ParsedSpecs
-
- toString() -
Method in class escjava.ast.QuantifiedExpr
-
- toString() -
Method in class escjava.ast.ReachModifierPragma
-
- toString() -
Method in class escjava.ast.RefinePragma
-
- toString() -
Method in class escjava.ast.ResExpr
-
- toString() -
Method in class escjava.ast.RestoreFromCmd
-
- toString() -
Method in class escjava.ast.SeqCmd
-
- toString() -
Method in class escjava.ast.SetCompExpr
-
- toString() -
Method in class escjava.ast.SetStmtPragma
-
- toString() -
Method in class escjava.ast.SimpleCmd
-
- toString() -
Method in class escjava.ast.SimpleModifierPragma
-
- toString() -
Method in class escjava.ast.SimpleStmtPragma
-
- toString() -
Method in class escjava.ast.SkolemConstantPragma
-
- toString() -
Method in class escjava.ast.Spec
-
- toString() -
Method in class escjava.ast.StillDeferredDeclPragma
-
- toString() -
Method in class escjava.ast.SubGetsCmd
-
- toString() -
Method in class escjava.ast.SubSubGetsCmd
-
- toString() -
Method in class escjava.ast.SubstExpr
-
- toString(int) -
Static method in class escjava.ast.TagConstants
-
- toString() -
Method in class escjava.ast.TypeExpr
-
- toString() -
Method in class escjava.ast.VarDeclModifierPragma
-
- toString() -
Method in class escjava.ast.VarExprModifierPragma
-
- toString() -
Method in class escjava.ast.VarExprModifierPragmaVec
-
- toString() -
Method in class escjava.ast.VarInCmd
-
- toString() -
Method in class escjava.ast.WildRefExpr
-
- toString() -
Method in class escjava.gui.GUI.GFCUTreeValue
-
- toString() -
Method in class escjava.gui.GUI.IETreeValue
-
- toString() -
Method in class escjava.gui.GUI.RDTreeValue
-
- toString() -
Method in class escjava.gui.GUI.TDTreeValue
-
- toString() -
Method in class escjava.pa.generic.Disjunction
-
- toString() -
Method in class escjava.prover.Atom
- Return the interned
String for the symbol we
represent.
- toString() -
Method in class escjava.prover.Formula
-
- toString() -
Method in class escjava.prover.SExp
-
- toString() -
Method in class escjava.prover.Signature
-
- toString() -
Method in class escjava.prover.SimplifyOutput
-
- toString() -
Method in class escjava.prover.SimplifyOutputSentinel
-
- toString() -
Method in class escjava.prover.SimplifyResult
-
- toString() -
Method in class escjava.prover.TriggerlessQuantWarning
-
- toString() -
Method in class escjava.translate.ATarget
-
- toString() -
Method in class escjava.vcGeneration.PrettyPrinter
-
- toString() -
Method in class escjava.vcGeneration.TNode
-
- toString() -
Method in class javafe.InputEntry
-
- toString() -
Method in class javafe.ast.ASTDecoration
- Return the name associated with
this.
- toString(ASTNode) -
Method in class javafe.ast.ASTDecoration
- Return a string containing the decoration's name, and the
decoration value for this
ASTNode.
- toString() -
Method in class javafe.ast.ASTNode
- Return a string representation of
this.
- toString() -
Method in class javafe.ast.AmbiguousMethodInvocation
-
- toString() -
Method in class javafe.ast.AmbiguousVariableAccess
-
- toString() -
Method in class javafe.ast.ArrayInit
-
- toString() -
Method in class javafe.ast.ArrayRefExpr
-
- toString() -
Method in class javafe.ast.ArrayType
-
- toString() -
Method in class javafe.ast.AssertStmt
-
- toString() -
Method in class javafe.ast.BinaryExpr
-
- toString() -
Method in class javafe.ast.BlockStmt
-
- toString() -
Method in class javafe.ast.BreakStmt
-
- toString() -
Method in class javafe.ast.CastExpr
-
- toString() -
Method in class javafe.ast.CatchClause
-
- toString() -
Method in class javafe.ast.CatchClauseVec
-
- toString() -
Method in class javafe.ast.ClassDecl
-
- toString() -
Method in class javafe.ast.ClassDeclStmt
-
- toString() -
Method in class javafe.ast.ClassLiteral
-
- toString() -
Method in class javafe.ast.CompilationUnit
-
- toString() -
Method in class javafe.ast.CompoundName
-
- toString() -
Method in class javafe.ast.CondExpr
-
- toString() -
Method in class javafe.ast.ConstructorDecl
-
- toString() -
Method in class javafe.ast.ConstructorInvocation
-
- toString() -
Method in class javafe.ast.ContinueStmt
-
- toString(int) -
Method in class javafe.ast.DelegatingPrettyPrint
-
- toString() -
Method in class javafe.ast.DoStmt
-
- toString() -
Method in class javafe.ast.ErrorType
-
- toString() -
Method in class javafe.ast.EvalStmt
-
- toString() -
Method in class javafe.ast.ExprObjectDesignator
-
- toString() -
Method in class javafe.ast.ExprVec
-
- toString() -
Method in class javafe.ast.FieldAccess
-
- toString() -
Method in class javafe.ast.FieldDecl
-
- toString() -
Method in class javafe.ast.FieldDeclVec
-
- toString() -
Method in class javafe.ast.ForStmt
-
- toString() -
Method in class javafe.ast.FormalParaDecl
-
- toString() -
Method in class javafe.ast.FormalParaDeclVec
-
- toString(int) -
Static method in class javafe.ast.GeneratedTags
-
- toString() -
Method in class javafe.ast.Identifier
- Return a string containing the symbol associated with
this.
- toString() -
Method in class javafe.ast.IdentifierNode
-
- toString() -
Method in class javafe.ast.IdentifierVec
-
- toString() -
Method in class javafe.ast.IfStmt
-
- toString() -
Method in class javafe.ast.ImportDeclVec
-
- toString() -
Method in class javafe.ast.InitBlock
-
- toString() -
Method in class javafe.ast.InstanceOfExpr
-
- toString() -
Method in class javafe.ast.InterfaceDecl
-
- toString() -
Method in class javafe.ast.JavafePrimitiveType
-
- toString() -
Method in class javafe.ast.LabelStmt
-
- toString() -
Method in class javafe.ast.LexicalPragmaVec
-
- toString() -
Method in class javafe.ast.LiteralExpr
-
- toString() -
Method in class javafe.ast.LocalVarDecl
-
- toString() -
Method in class javafe.ast.MethodDecl
-
- toString() -
Method in class javafe.ast.MethodDeclVec
-
- toString() -
Method in class javafe.ast.MethodInvocation
-
- toString() -
Method in class javafe.ast.ModifierPragmaVec
-
- toString(int) -
Static method in class javafe.ast.Modifiers
-
- toString() -
Method in class javafe.ast.NewArrayExpr
-
- toString() -
Method in class javafe.ast.NewInstanceExpr
-
- toString() -
Method in class javafe.ast.OnDemandImportDecl
-
- toString(int) -
Static method in class javafe.ast.OperatorTags
-
- toString() -
Method in class javafe.ast.ParenExpr
-
- toString(int) -
Method in class javafe.ast.PrettyPrint
-
- toString(TypeNameVec) -
Method in class javafe.ast.PrettyPrint
-
- toString(FormalParaDeclVec) -
Method in class javafe.ast.PrettyPrint
-
- toString(ExprVec) -
Method in class javafe.ast.PrettyPrint
-
- toString(GenericVarDecl) -
Method in class javafe.ast.PrettyPrint
-
- toString(LocalVarDecl, boolean) -
Method in class javafe.ast.PrettyPrint
-
- toString(FieldDecl, boolean) -
Method in class javafe.ast.PrettyPrint
-
- toString(Type) -
Method in class javafe.ast.PrettyPrint
-
- toString(Name) -
Method in class javafe.ast.PrettyPrint
-
- toString(VarInit) -
Method in class javafe.ast.PrettyPrint
-
- toString(ObjectDesignator) -
Method in class javafe.ast.PrettyPrint
-
- toString() -
Method in class javafe.ast.ReturnStmt
-
- toString() -
Method in class javafe.ast.SimpleName
-
- toString() -
Method in class javafe.ast.SingleTypeImportDecl
-
- toString() -
Method in class javafe.ast.SkipStmt
-
- toString() -
Method in class javafe.ast.StmtVec
-
- toString() -
Method in class javafe.ast.SuperObjectDesignator
-
- toString() -
Method in class javafe.ast.SwitchLabel
-
- toString() -
Method in class javafe.ast.SwitchStmt
-
- toString() -
Method in class javafe.ast.SynchronizeStmt
-
- toString(int) -
Static method in class javafe.ast.TagConstants
-
- toString() -
Method in class javafe.ast.ThisExpr
-
- toString() -
Method in class javafe.ast.ThrowStmt
-
- toString() -
Method in class javafe.ast.TryCatchStmt
-
- toString() -
Method in class javafe.ast.TryFinallyStmt
-
- toString() -
Method in class javafe.ast.TypeDeclElemVec
-
- toString() -
Method in class javafe.ast.TypeDeclVec
-
- toString() -
Method in class javafe.ast.TypeModifierPragmaVec
-
- toString() -
Method in class javafe.ast.TypeName
-
- toString() -
Method in class javafe.ast.TypeNameVec
-
- toString() -
Method in class javafe.ast.TypeObjectDesignator
-
- toString() -
Method in class javafe.ast.UnaryExpr
-
- toString() -
Method in class javafe.ast.VarDeclStmt
-
- toString() -
Method in class javafe.ast.VarInitVec
-
- toString() -
Method in class javafe.ast.VariableAccess
-
- toString() -
Method in class javafe.ast.WhileStmt
-
- toString(int) -
Static method in class javafe.parser.TagConstants
-
- toString(int) -
Static method in class javafe.tc.TagConstants
-
- toString() -
Method in class javafe.tc.TypeSig
- Returns a String that represents the value of this Object.
- toString() -
Method in class javafe.tc.TypeSigVec
-
- toString(int) -
Static method in class javafe.util.Location
- Convert a location into a printable description suitable for use
in a warning or error message.
- toString() -
Method in class javafe.util.LocationManagerCorrelatedReader
-
- toString() -
Method in class javafe.util.Set
-
- toString() -
Method in class javafe.util.StackVector
-
- toStrings(int) -
Method in class javafe.ast.CompoundName
-
- toStrings(int) -
Method in class javafe.ast.Name
- Return the first
len identifiers in
this in an array.
- toStrings() -
Method in class javafe.ast.Name
- Return all identifiers in
this in an array.
- toStrings(int) -
Method in class javafe.ast.SimpleName
-
- toVcString(int) -
Static method in class escjava.ast.TagConstants
-
- tokenType -
Variable in class javafe.ast.Identifier
- This field defaults to
TagConstants.IDENT, but
is set to other values by the scanner to indicate keywords.
- toks -
Variable in class javafe.parser.TokenQueue
- Contents of queue tokens.
- topNode -
Static variable in class escjava.gui.GUI
-
- totalLinesRead -
Static variable in class javafe.util.LocationManagerCorrelatedReader
- The total # of lines that have been read so far by all
FileCorrelatedReaders.
- tr(String, char, char) -
Static method in class javafe.filespace.Resolve
- Convert 1 character to another everywhere it appears in a given
string.
- trAndGen(Expr) -
Method in class escjava.translate.DefGCmd
- (new trAndGent)
- trBody(RoutineDecl, FindContributors, Hashtable, Set, Translate, boolean) -
Method in class escjava.translate.Translate
- Translates the body of a method or constructor, as described in ESCJ 16, section
8.
- trConstructorBody(ConstructorDecl, Hashtable) -
Method in class escjava.translate.Translate
- Auxiliary routine used by trBody to translate the body of a constructor, as
described in ESCJ 16, section 8.
- trConstructorCallStmt(ConstructorInvocation) -
Method in class escjava.translate.Translate
- This method implements "TrConstructorCallStmt" as described in section 6 of
ESCJ 16.
- trExpr(boolean, VarInit) -
Method in class escjava.translate.Translate
- Translate
expr into a sequence of guarded commands that are
appended to code and return an expression denoting the value of
the expression.
- trFieldAccess(boolean, FieldAccess) -
Method in class escjava.translate.Translate
- Returns either a
VariableAccess if fa is a class
variable or a SELECT application if fa is an
instance variable access, or an ARRAYLENGTH application if
fa is the final array field length.
- trIfStmt(Expr, Stmt, Stmt, TypeDecl) -
Method in class escjava.translate.Translate
- Translate an "if" statement.
- trMethodDecl(DerivedMethodDecl, Hashtable) -
Static method in class escjava.translate.GetSpec
- Translates a MethodDecl to a Spec.
- trMethodDeclPostcondition(DerivedMethodDecl, Hashtable, ExprVec) -
Static method in class escjava.translate.GetSpec
- Computes the postconditions, according to section 7.2.2 of ESCJ 16.
- trMethodDeclPreconditions(DerivedMethodDecl, ExprVec) -
Static method in class escjava.translate.GetSpec
- Computes the preconditions, according to section 7.2.0 of ESCJ 16.
- trMethodInvocation(boolean, MethodInvocation) -
Method in class escjava.translate.Translate
- This translation of method invocation follows section 4.1 of ESCJ 16.
- trSpecAuxAxiomsNeeded -
Static variable in class escjava.translate.TrAnExpr
-
- trSpecExpr(Expr) -
Static method in class escjava.translate.TrAnExpr
- This is the abbreviated form of function
TrSpecExpr
described in ESCJ 16.
- trSpecExpr(Expr, Expr) -
Static method in class escjava.translate.TrAnExpr
-
- trSpecExpr(Expr, Hashtable, Hashtable, Expr) -
Static method in class escjava.translate.TrAnExpr
-
- trSpecExpr(Expr, Hashtable, Hashtable) -
Static method in class escjava.translate.TrAnExpr
-
- trSpecExprAuxAssumptions -
Static variable in class escjava.translate.TrAnExpr
-
- trSpecExprAuxConditions -
Static variable in class escjava.translate.TrAnExpr
-
- trSpecExprI(Expr, Hashtable, Hashtable) -
Method in class escjava.translate.TrAnExpr
-
- trSpecModelVarsUsed -
Static variable in class escjava.translate.TrAnExpr
-
- trStmt(Stmt, TypeDecl) -
Method in class escjava.translate.Translate
- Translate
stmt into a sequence of guarded commands
that are appended to code.
- trSynchronizedBody(Expr, Stmt, int, TypeDecl) -
Method in class escjava.translate.Translate
-
- trType(Type) -
Static method in class escjava.translate.TrAnExpr
-
- traceInfo -
Variable in class escjava.Options
-
- traceInfoLabelCmd(ASTNode, String) -
Method in class escjava.translate.Translate
-
- traceInfoLabelCmd(ASTNode, String, int) -
Method in class escjava.translate.Translate
-
- traceInfoLabelCmd(int, int, String, int) -
Method in class escjava.translate.Translate
-
- traceInfoLabelCmd(int, int, String, String) -
Method in class escjava.translate.Translate
-
- traceMethod() -
Method in class escjava.translate.DefGCmd
-
- trackReadChars -
Variable in class escjava.Options
-
- transition(TypeSig) -
Static method in class javafe.tc.SLResolution
- Transition
sig to the supertype-links-resolved
state.
- translate -
Static variable in class escjava.translate.TrAnExpr
-
- translateDecoration -
Static variable in class escjava.translate.Purity
- Decorates
VarInit nodes with purity information.
- translator -
Variable in class escjava.translate.Frame
- The Translate instance that owns this instance of Frame
- traverse(ASTNode) -
Method in class escjava.translate.CalcFreeVars
-
- tree -
Static variable in class escjava.gui.EscFrame
-
- treeModel -
Static variable in class escjava.gui.GUI
-
- treeView -
Variable in class escjava.gui.EscFrame
-
- trim(VarInit) -
Method in class escjava.translate.Translate
- Peels off parentheses and casts from
E and returns the result
- trimNewlines(String) -
Static method in class escjava.prover.SubProcess
-
- trim_whitespace(String) -
Static method in class javafe.filespace.StringUtil
- Remove leading and trailing whitespace (just spaces for now):
- truelit -
Static variable in class escjava.translate.GC
-
- tryClause -
Variable in class javafe.ast.TryCatchStmt
-
- tryClause -
Variable in class javafe.ast.TryFinallyStmt
-
- tryCondExprMatch(Expr, Expr) -
Method in class javafe.tc.FlowInsensitiveChecks
- Return the type of a E1 : L ?
- trycmd(GuardedCmd, GuardedCmd) -
Static method in class escjava.translate.GC
-
- ttype -
Variable in class escjava.parser.EscPragmaParser.SavedPragma
-
- ttype -
Variable in class javafe.parser.Token
- Integer code giving the kind of token.
- type -
Variable in class escjava.ast.SetCompExpr
-
- type -
Variable in class escjava.ast.TypeExpr
-
- type() -
Method in class escjava.gui.GUI.EscTreeValue
-
- type() -
Method in class escjava.gui.GUI.GFCUTreeValue
-
- type() -
Method in class escjava.gui.GUI.IETreeValue
-
- type() -
Method in class escjava.gui.GUI.RDTreeValue
-
- type() -
Method in class escjava.gui.GUI.TDTreeValue
-
- type(Type) -
Static method in class escjava.translate.UniqName
- Returns the unique-ification of the type
t.
- type -
Variable in class escjava.vcGeneration.TNode
-
- type -
Variable in class escjava.vcGeneration.VariableInfo
-
- type() -
Method in class javafe.ClassInputEntry
-
- type() -
Method in class javafe.DirInputEntry
-
- type() -
Method in class javafe.FileInputEntry
-
- type() -
Method in class javafe.InputEntry
-
- type() -
Method in class javafe.ListInputEntry
-
- type() -
Method in class javafe.PackageInputEntry
-
- type() -
Method in class javafe.UnknownInputEntry
-
- type -
Variable in class javafe.ast.CastExpr
-
- type -
Variable in class javafe.ast.ClassLiteral
-
- type -
Variable in class javafe.ast.ExprObjectDesignator
-
- type() -
Method in class javafe.ast.ExprObjectDesignator
-
- type -
Variable in class javafe.ast.GenericVarDecl
-
- type -
Variable in class javafe.ast.InstanceOfExpr
-
- type -
Variable in class javafe.ast.NewArrayExpr
- The type of the elements being given zero-default values, or (if
an array initializer is present), the type of the array
initializer elements.
- type -
Variable in class javafe.ast.NewInstanceExpr
-
- type() -
Method in class javafe.ast.ObjectDesignator
-
- type -
Variable in class javafe.ast.SuperObjectDesignator
-
- type() -
Method in class javafe.ast.SuperObjectDesignator
-
- type -
Variable in class javafe.ast.TypeObjectDesignator
-
- type() -
Method in class javafe.ast.TypeObjectDesignator
-
- typeAndNonNullAllocCorrectAs(GenericVarDecl, Type, SimpleModifierPragma, boolean, Hashtable, boolean) -
Static method in class escjava.translate.TrAnExpr
- Returns a vector of conjuncts.
- typeAndNonNullCorrectAs(GenericVarDecl, Type, SimpleModifierPragma, boolean, Hashtable) -
Static method in class escjava.translate.TrAnExpr
-
- typeCorrect(GenericVarDecl) -
Static method in class escjava.translate.TrAnExpr
- This method implements the ESCJ 16 function
TypeCorrect.
- typeCorrect(GenericVarDecl, Hashtable) -
Static method in class escjava.translate.TrAnExpr
-
- typeCorrectAs(GenericVarDecl, Type) -
Static method in class escjava.translate.TrAnExpr
-
- typeDecl -
Variable in class escjava.translate.Translate
- The type containing the routine whose body is being translated.
- typeDecl -
Variable in class javafe.reader.ASTClassFileParser
- The AST of the class parsed by this parser.
- typeDecoration -
Static variable in class javafe.tc.FlowInsensitiveChecks
- Decorates
VarInit nodes to point to Type objects.
- typeEnv -
Static variable in class javafe.tc.Env
- decoration holding the type environment in which a type is resolved.
- typeExists(Tree, String) -
Static method in class javafe.filespace.Resolve
- Does a package contain a reference type with a given simple
name?
- typeExpr(Type) -
Static method in class escjava.translate.GC
-
- typeName(Type) -
Static method in class escjava.translate.Suggestion
-
- typeName -
Variable in class javafe.ast.SingleTypeImportDecl
-
- typeOption() -
Method in class javafe.ClassInputEntry
-
- typeOption() -
Method in class javafe.DirInputEntry
-
- typeOption() -
Method in class javafe.FileInputEntry
-
- typeOption() -
Method in class javafe.InputEntry
-
- typeOption() -
Method in class javafe.ListInputEntry
-
- typeOption() -
Method in class javafe.PackageInputEntry
-
- typeProofSet -
Static variable in class escjava.vcGeneration.TNode
-
- typeSigs() -
Method in class escjava.backpred.FindContributors
- Enumerate the TypeSig contributors
- typeSure -
Variable in class escjava.vcGeneration.VariableInfo
-
- typeTree() -
Method in class escjava.vcGeneration.TAllocLE
-
- typeTree() -
Method in class escjava.vcGeneration.TAllocLT
-
- typeTree() -
Method in class escjava.vcGeneration.TAnyEQ
-
- typeTree() -
Method in class escjava.vcGeneration.TAsField
-
- typeTree() -
Method in class escjava.vcGeneration.TBoolOp
-
- typeTree() -
Method in class escjava.vcGeneration.TCast
-
- typeTree() -
Method in class escjava.vcGeneration.TFClosedTime
-
- typeTree() -
Method in class escjava.vcGeneration.TFloatFun
-
- typeTree() -
Method in class escjava.vcGeneration.TFloatOp
-
- typeTree() -
Method in class escjava.vcGeneration.TFunction
-
- typeTree() -
Method in class escjava.vcGeneration.TIntFun
-
- typeTree() -
Method in class escjava.vcGeneration.TIntOp
-
- typeTree() -
Method in class escjava.vcGeneration.TIs
-
- typeTree() -
Method in class escjava.vcGeneration.TIsAllocated
-
- typeTree() -
Method in class escjava.vcGeneration.TMethodCall
-
- typeTree() -
Method in class escjava.vcGeneration.TName
-
- typeTree() -
Method in class escjava.vcGeneration.TNode
-
- typeTree() -
Method in class escjava.vcGeneration.TRefOp
-
- typeTree() -
Method in class escjava.vcGeneration.TRoot
-
- typeTree() -
Method in class escjava.vcGeneration.TSelect
-
- typeTree() -
Method in class escjava.vcGeneration.TStore
-
- typeTree() -
Method in class escjava.vcGeneration.TTypeOp
-
- typeTree() -
Method in class escjava.vcGeneration.TUnset
-
- typeTree() -
Method in class escjava.vcGeneration.TVariable
-
- typecheck(TypeSig) -
Method in class escjava.backpred.FindContributors
- Make sure a given TypeSig has been type checked, type checking
it if necessary.
- typecheck() -
Method in class javafe.tc.TypeSig
- Transition
this to the "checked" state.
- typecheckCaution -
Static variable in class escjava.ColorOptions
-
- typecheckComplete(int) -
Static method in class escjava.Status
-
- typecheckError -
Static variable in class escjava.ColorOptions
-
- typecheckOK -
Static variable in class escjava.ColorOptions
-
- typecheckRegisteredNowarns() -
Static method in class escjava.translate.NoWarn
- Type checks the registered nowarn pragmas, reporting errors to
ErrorSet appropriately.
- typecheckSuperTypes() -
Method in class javafe.tc.TypeSig
- Typecheck the superclass of the current classtype being typecheck and
typecheck all interfaces that the current classtype implements.
- typecodeType -
Static variable in class escjava.tc.Types
-
- typesName -
Static variable in class escjava.vcGeneration.TNode
- map containing all the types used in the proof.
GenericFiles that cannot
be opened. UsageError exception.
sub is a subtype of
the universe modifier sup.
System.err.
System.err.
int we represent.
v.
VariableInfo(oldName, type) associated as value.
True or False.
myvar = true
declaredLocals and code and then appends
code with a VARINCMD (if there were any new declared locals) or a
sequence of commands (otherwise).
byte to this output stream.
byte to this output stream.
b.length bytes to this output stream.
len bytes from the specified
byte array starting at offset off to
this output stream.
this suitable for debug
output.
Token fields
haven't been mucked with by outside code).
this.
_SpecialParserInterface is not a class that should be
used by general clients of the javafe.ast package.
|
ESC/Java2 © 2003,2004,2005,2006 David Cok and Joseph Kiniry © 2005,2006 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 | ||||||||||