|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV NEXT | FRAMES NO FRAMES |
ASTNode
.
ASTDecoration
object with the given
name.
ASTNode
is the root of the abstract syntax tree node
hierarchy. javafe.ast
. Atom
s 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.
- add2Decl(String) -
Static method in class escjava.translate.VcToStringPvs
-
- add2DeclFun(String, int) -
Static method in class escjava.translate.VcToStringPvs
-
- 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
-
- 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
-
- 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.
- 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(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
-
- 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 -
Variable in class junitutils.Diff
- This is set to true if the oldText and newText are not the same
- 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() -
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
-
- argumentFileNames -
Variable in class javafe.CopyLoaded
-
- 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 TypeDecl
s
inside a CompilationUnit
to point to that unit.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
.
setType
on x
before its
done.
fd
into implementation checked state.
CompilationUnit to make sure that each import is
individually well formed.
- checkInit(Env, VarInit, Type) -
Method in class javafe.tc.FlowInsensitiveChecks
-
- checkIntegralType(Expr) -
Static method in class javafe.tc.FlowInsensitiveChecks
-
- 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
-
- 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
Modifier
s.
- checkModifierPragmaVec(ModifierPragmaVec, ASTNode, Env) -
Method in class javafe.tc.FlowInsensitiveChecks
- Hook to do additional processing on
ModifierVec
s.
- 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
-
- 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.
- 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
-
- 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
-
- 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.
- 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.
- 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.
- 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.
- checkUses(Expr, Set, Set, Set) -
Static method in class escjava.translate.GCSanity
-
- 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.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.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.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.PrimitiveType
-
- 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.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.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.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.PrimitiveType
-
- 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() -
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.PPOutputStream
- Closes this output stream and releases any system resources
associated with the stream.
- 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.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.
- 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
-
- combinedString() -
Method in class escjava.gui.GUI.EscTreeValue
-
- combinedString() -
Method in class escjava.gui.GUI.RDTreeValue
-
- 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
).
- 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
.
- compute(Expr, PrintStream) -
Static method in class escjava.translate.VcToStringPvs
- 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
-
- computePC(Expr, PrintStream) -
Static method in class escjava.translate.VcToStringPvs
-
- computeTypeSpecific(Expr, PrintStream) -
Static method in class escjava.translate.VcToString
- Prints
e
as a simple-expression string to to
.
- computeTypeSpecific(Expr, PrintStream) -
Static method in class escjava.translate.VcToStringPvs
- 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
-
- 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
-
- copySourceFile(String, String) -
Method in class javafe.CopyLoaded
- Copy the source file original into the file newName.
- 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
-
- 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.
- 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
-
- 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
-
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.
n
th 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.
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
MethodDecl
s 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
MethodDecl
s that a given
MethodDecl
overrides or hides.
- getAllSpecs(RoutineDecl) -
Static method in class escjava.ast.Utils
-
- 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.
- 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
-
- getDefpreds(Expr) -
Method in class escjava.translate.VcToStringPvs
-
- getDefpredsHelper(Expr) -
Method in class escjava.translate.VcToString
-
- getDefpredsHelper(Expr) -
Method in class escjava.translate.VcToStringPvs
-
- getDirectOverrides(MethodDecl) -
Static method in class escjava.tc.FlowInsensitiveChecks
-
- getDoubleConstant(Object) -
Static method in class javafe.tc.ConstantExpr
-
- 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 intermost 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.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
MethodDecl
s that a given
class MethodDecl
implements.
- getImplementsSet(MethodDecl) -
Method in class javafe.tc.TypeCheck
- Retrieves the set of interface
MethodDecl
s 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.
- 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.
- 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(RoutineDecl) -
Method in class javafe.tc.TypeCheck
- Returns the user-readable name for a
RoutineDecl
.
- 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
-
- getNonNull(RoutineDecl) -
Method in class escjava.AnnotationHandler
-
- 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
-
- 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
.
- 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.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.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(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.
- 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
.
- 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
Name
s that are equals
have the same hash
code.
this
such that two
Name
s that are equals
have the same
hash code.
this
such that two
Name
s 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
.
insideNoPats
is really a parameter to *
printTerm
.
instanceInitializers
.
integralPrintName
by symbolic
names.
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
-
- 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.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
-
- 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 GenericFile
s 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.
CompilationUnit
s 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.
String
s to already created
non-null Atom
s.
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.
TypeDeclElem
s
inside the this
.
TypeDeclElems
s
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
.
Type
s 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
.
SList
s 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
.
computeTypeSpecific
.
this
to the supertype links resolved
state.
CorrelatedReader
.
map
restricted to the
domain e
.
args
are the
command-line arguments we have been invoked with.
SInt
representing a given
int
.
SList
s represent possibly-empty lists of
SExp
s.
SList
may not be extended outside this package.
SNil
instance represents the empty list of
SExp
s.SPair
is a pair of a SExp
and a
SList
; together with the SNil
class, it is
used to implement lists of SExp
s. 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 CompilationUnit
s
found in source files. TypeReader
that uses SlowQuery
to find type files, and user-supplied
Reader
s 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
.
i
th element to
s
.
init
with d
; will be returned by a call
to getInitVar
.
Listener
to be notified about
CompilationUnit
loading.
cu
.
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
.
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
.
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 OutputStream
s. - 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() -
Constructor for class javafe.ast.ThisExpr
- Construct a raw ThisExpr whose class invariant(s) have not
yet been established.
- ThrowStmt - class javafe.ast.ThrowStmt.
-
- ThrowStmt() -
Constructor for class javafe.ast.ThrowStmt
- Construct a raw ThrowStmt whose class invariant(s) have not
yet been established.
- 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() -
Constructor for class javafe.ast.TryCatchStmt
- Construct a raw TryCatchStmt whose class invariant(s) have not
yet been established.
- TryFinallyStmt - class javafe.ast.TryFinallyStmt.
-
- TryFinallyStmt() -
Constructor for class javafe.ast.TryFinallyStmt
- Construct a raw TryFinallyStmt whose class invariant(s) have not
yet been established.
- Type - class javafe.ast.Type.
- Represents a Type syntactic unit.
- Type() -
Constructor for class javafe.ast.Type
- Construct a raw Type whose class invariant(s) have not
yet been established.
- 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() -
Constructor for class javafe.ast.TypeDecl
- Construct a raw TypeDecl whose class invariant(s) have not
yet been established.
- TypeDeclElem - interface javafe.ast.TypeDeclElem.
- Represents either a ClassBodyDeclaration or an
InterfaceMemberDeclaration.
- TypeDeclElemPragma - class javafe.ast.TypeDeclElemPragma.
-
- TypeDeclElemPragma() -
Constructor for class javafe.ast.TypeDeclElemPragma
- Construct a raw TypeDeclElemPragma whose class invariant(s) have not
yet been established.
- 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() -
Constructor for class escjava.ast.TypeExpr
- Construct a raw TypeExpr whose class invariant(s) have not
yet been established.
- TypeModifierPragma - class javafe.ast.TypeModifierPragma.
-
- TypeModifierPragma() -
Constructor for class javafe.ast.TypeModifierPragma
- Construct a raw TypeModifierPragma whose class invariant(s) have not
yet been established.
- 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() -
Constructor for class javafe.ast.TypeName
- Construct a raw TypeName whose class invariant(s) have not
yet been established.
- 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() -
Constructor for class javafe.ast.TypeObjectDesignator
- Construct a raw TypeObjectDesignator whose class invariant(s) have not
yet been established.
- 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.
-
- 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).
- 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.
- 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.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.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 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.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.PrimitiveType
-
- 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.
- 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
-
- 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() -
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
-
- typeSigs() -
Method in class escjava.backpred.FindContributors
- Enumerate the TypeSig contributors
- 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
-
GenericFile
s that cannot
be opened. UsageError
exception.
System.err
.
System.err
.
int
we represent.
v
.
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.
b.length
bytes 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 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV NEXT | FRAMES NO FRAMES |