Uses of Class
org.jmlspecs.checker.JmlSourceClass

Packages that use JmlSourceClass

org.jmlspecs.checker

Contains the source code for a parser and typechecker for JML annotations and java code.

Uses of JmlSourceClass in org.jmlspecs.checker

Subclasses of JmlSourceClass in org.jmlspecs.checker

class

JmlBinarySourceClass This class represents a class read from a *.class file.

Fields in org.jmlspecs.checker declared as JmlSourceClass

protected JmlSourceClass	JmlSourceClass.refinedSourceClass This field contains the source class of the type declaration that is refined by the current type; it is used when looking up names such as fields or classes.
protected JmlSourceClass	JmlSourceClass.refiningSourceClass

Methods in org.jmlspecs.checker that return JmlSourceClass

JmlSourceClass	JmlSourceClass.getRefinedType() Returns the refined 'JmlSourceClass' for this class
JmlSourceClass	JmlSourceClass.getRefiningType() Returns the refining 'JmlSourceClass' for this class
JmlSourceClass	JmlSourceClass.getMostRefined()
JmlSourceClass	JmlSourceClass.lookupRefinedInnerType(CClass specType) Searches for the inner type refined by a given inner type, looking in the refinement hierarchy as needed.

Methods in org.jmlspecs.checker with parameters of type JmlSourceClass

void	JmlSourceClass.checkFileNameAndSuffix(JmlSourceClass refinedType) This method ensures that a file at a lower level only refines a file at the same or higher level; but this check is only done on the most refined definition of a class.
boolean	JmlSourceClass.isMoreRefinedThan(JmlSourceClass j) Returns true if the calling object is more refined (perhaps in more than one step) than the argument; Returns false if they are the same object or the calling argument is less refined or they are not part of the same refinement seqeuence.
void	JmlSourceClass.setRefinedType(JmlSourceClass refinedType) Sets the refinedType field of this JmlSourceClass object.
protected int	JmlSourceClass.compareLevelsTo(JmlSourceClass other)
void	JmlAssignableClause.precheckStoreRefs(JmlSourceClass methodOwner)
static CFlowControlContextType	JmlContext.createDummyContext(JmlSourceClass self)
protected void	JmlTypeLoader.loadMostRefinedType(JmlSourceClass sourceClass) Loads the "most refined" source class of this type.