Uses of Class
org.jmlspecs.checker.JmlContext

Packages that use JmlContext

org.jmlspecs.checker

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

Uses of JmlContext in org.jmlspecs.checker

Subclasses of JmlContext in org.jmlspecs.checker

class	JmlClassContext This class represents the context for a class during checking passes (checkInterface, checkInitializers, typecheck).
class	JmlCompilationUnitContext This class represents the context for a compilation unit during checking passes (checkInterface, checkInitializers, typecheck).
class	JmlConstructorContext This class represents the context for a constructor during checking passes (checkInterface, checkInitializers, typecheck).
class	JmlExpressionContext A class for representing the context in which JML expressions are typechecked.
class	JmlFlowControlContext This class is used during typechecking for control flow analysis that maintains local variable definite assignment (JLS2, 16), throwable, and reachability information (JLS2, 14.20).
class	JmlInitializerContext This class represents the context for a static initializer during checking passes (checkInterface, checkInitializers, typecheck).
class	JmlInterfaceContext This class represents the context for an interface declaration during checking passes (checkInterface, checkInitializers, typecheck).
class	JmlMethodContext This class represents the context for a method during checking passes (checkInterface, checkInitializers, typecheck).

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

private void	JmlMethodDeclaration.accumulateNonNullStats(JmlContext context)
static void	NonNullStatistics.checkExpression(JExpression j, JmlContext context, String fn, int clause, boolean ifNot, boolean ifInvStatic)
static void	NonNullStatistics.checkSpecification(JmlMethodDeclaration jmd, Object[] jscArr, JmlContext context, String fn)
static void	NonNullStatistics.checkSpecCase(JmlSpecCase jsc, JmlContext context, String fn, boolean fromHeavy)
static void	NonNullStatistics.checkSpecBody(JmlSpecBody jsb, JmlContext context, String fn)
static void	NonNullStatistics.checkSpecBodyClause(JmlSpecBodyClause jsbc, JmlContext context, String fn)
private static void	NonNullStatistics.handleNNElementExpr(JmlNonNullElementsExpression j, JmlContext context, String fn, int clause, boolean ifInvStatic)
private static void	NonNullStatistics.handleInstanceofExpression(JInstanceofExpression j, JmlContext context, String fn, int clause, boolean ifInvStatic)
private static void	NonNullStatistics.handleEqualityExpression(JmlEqualityExpression je, JmlContext context, String fn, int clause, boolean ifNot, boolean ifInvStatic)
private static void	NonNullStatistics.handleFreshExpression(JmlFreshExpression jf, JmlContext context, int clause, String fn)
static void	NonNullStatistics.handleMethodDeclaration(JmlMethodDeclaration jmd, JMethodDeclaration delegee, String fileName, JmlContext context)