Package escjava.translate

Class Summary

AssocDeclClipPolicy
ATarget	Infers more precise loop targets.
AuxInfo
AuxInfoLink
CalcFreeVars
DefGCmd	Class DefGCmd implements the definedness guarded commands for the requires clauses.
Ejp
ErrorMsg	Provides printing of error messages to the user.
Frame
Frame.ModifiesIterator	This class enables iterating over the set of store-ref locations in a ModifiesGroupPragma.
GC
GCSanity
GetSpec	Responsible for getting Spec for calls.
Helper
InitialState	This class provides two methods used in the generation of a verification condition for a method or constructor (see section 8 of ESCJ 16).
InlineConstructor
InlineSettings
Inner	* This class contains a number of routines used in the * interpretation of Java 1.1 as Java 1.0
InvariantInfo	* This class is used by collectInvariants and its callers, * extendSpecForCall and extendSpecForBody.
LabelInfoToString
NoWarn	Handles turning off warnings.
ParamAndGlobalVarInfo	This class is used by collectParamsAndGlobalVars and its * caller, extendSpecForCall.
Purity
RepHelper
Substitute	Responsible for performing substitutions in expressions.
Substitute.SetRef
Suggestion	This class generates possible ways to annotate a program to eliminate a given warning.
Targets	Provides methods for computing various kinds of syntactic targets
TrAnExpr	Translates Annotation Expressions to GCExpr.
Translate
Translate.Strings
UniqName	This class provides methods for unique-ifying names, as described in ESCJ 23b, "Unique names in ESC/Java".
VcToString