Uses of Class
org.jmlspecs.checker.JmlExpressionContext

Packages that use JmlExpressionContext

org.jmlspecs.checker

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

Uses of JmlExpressionContext in org.jmlspecs.checker

Fields in org.jmlspecs.checker declared as JmlExpressionContext

protected JmlExpressionContext

JmlAdmissibilityVisitor.ectx The context of the expression to check

Methods in org.jmlspecs.checker that return JmlExpressionContext

protected JmlExpressionContext	JmlDeclaration.createContext(CContextType context) Create a JmlExpressionContext object as a child of the given (CClassContextType) context that can be used to typecheck this JML declaration.
protected JmlExpressionContext	JmlConstraint.createContext(CContextType context) Create a JmlExpressionContext object as a child of the given (CClassContextType) context that can be used to typecheck this JML declaration.
protected JmlExpressionContext	JmlAxiom.createContext(CContextType context) Create a JmlExpressionContext object as a child of the given (CClassContextType) context, which is suitable for checking this axiom clause.
protected abstract JmlExpressionContext	JmlPredicateClause.createContext(CFlowControlContextType context) Returns an appropriate context for checking this clause.
protected JmlExpressionContext	JmlRequiresClause.createContext(CFlowControlContextType context) Returns an appropriate context for checking this clause.
protected JmlExpressionContext	JmlSpecStatementClause.createContext(CFlowControlContextType context) Returns an appropriate context for checking this clause.
protected JmlExpressionContext	JmlDivergesClause.createContext(CFlowControlContextType context) Returns an appropriate context for checking this clause.
protected JmlExpressionContext	JmlDurationClause.createContext(CFlowControlContextType context) Returns an appropriate context for checking this clause.
protected JmlExpressionContext	JmlEnsuresClause.createContext(CFlowControlContextType context) Returns an appropriate context for checking this clause.
protected JmlExpressionContext	JmlMeasuredClause.createContext(CFlowControlContextType context) Returns an appropriate context for checking this clause.
protected JmlExpressionContext	JmlReturnsClause.createContext(CFlowControlContextType context) Returns an appropriate context for checking this clause.
protected JmlExpressionContext	JmlSignalsOnlyClause.createContext(CFlowControlContextType context) Returns an appropriate context for checking this clause.
protected JmlExpressionContext	JmlSignalsClause.createContext(CFlowControlContextType context) Returns an appropriate context for checking this clause.
protected JmlExpressionContext	JmlSpecStatement.createContext(CFlowControlContextType context) Returns an appropriate context for checking this clause.
protected JmlExpressionContext	JmlWhenClause.createContext(CFlowControlContextType context) Returns an appropriate context for checking this clause.
protected JmlExpressionContext	JmlWorkingSpaceClause.createContext(CFlowControlContextType context) Returns an appropriate context for checking this clause.
static JmlExpressionContext	JmlExpressionContext.createPrecondition(CFlowControlContextType parent) Create and return a precondition context.
static JmlExpressionContext	JmlExpressionContext.createPostcondition(CFlowControlContextType parent) Create and return a normal postcondition context.
static JmlExpressionContext	JmlExpressionContext.createExceptionalPostcondition(CFlowControlContextType parent) Create and return an exceptional postcondition context.
static JmlExpressionContext	JmlExpressionContext.createWorkingSpace(CFlowControlContextType parent) Create and return a working_space context.
static JmlExpressionContext	JmlExpressionContext.createDuration(CFlowControlContextType parent) Create and return a duration context.
static JmlExpressionContext	JmlExpressionContext.createInternalCondition(CFlowControlContextType parent) Create and return an internal condition context.
static JmlExpressionContext	JmlExpressionContext.createOldExpression(CFlowControlContextType parent) Create and return an old expression context.
static JmlExpressionContext	JmlExpressionContext.createIntracondition(CFlowControlContextType parent) Create and return an intracondition context.
static JmlExpressionContext	JmlExpressionContext.createIntercondition(CFlowControlContextType parent) Create and return an intercondition context.
static JmlExpressionContext	JmlExpressionContext.createSameKind(CFlowControlContextType parent, JmlExpressionContext ctx) Return a new JmlExpressionContext of the same kind as the given argument ctx.

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

protected void	JmlRepresentsDecl.checkStoreRef(JmlExpressionContext context) Checks the store ref of this depends/represents clause.
protected void	JmlRepresentsDecl.checkRightHandSide(JmlExpressionContext context) Performs type-checking of right-hand side of the represents clause.
static boolean	JmlAdmissibilityVisitor.checkInvariant(JmlInvariant expr, JmlExpressionContext ectx) Admissibility checks an invariant.
static boolean	JmlAdmissibilityVisitor.checkRepresentsClause(JmlRepresentsDecl decl, JmlExpressionContext ectx) Admissibility checks a represents clause.
protected static boolean	JmlAdmissibilityVisitor.checkAdmissibility(JExpression expr, JmlExpressionContext ectx, CFieldAccessor modelField) Admissibility checks a JExpression.
static JmlExpressionContext	JmlExpressionContext.createSameKind(CFlowControlContextType parent, JmlExpressionContext ctx) Return a new JmlExpressionContext of the same kind as the given argument ctx.

Constructors in org.jmlspecs.checker with parameters of type JmlExpressionContext

JmlExpressionContext(JmlExpressionContext parent)