Uses of Class
org.jmlspecs.checker.JmlSpecExpression

Packages that use JmlSpecExpression

org.jmlspecs.checker	Contains the source code for a parser and typechecker for JML annotations and java code.
org.jmlspecs.jmldoc.jmldoc_142
org.jmlspecs.jmlrac	Generates Java classes from JML specifications that check assertions at runtime.
org.jmlspecs.jmlrac.qexpr	Translates JML quantified expressions into Java source code to evaluate them at runtime.

Uses of JmlSpecExpression in org.jmlspecs.checker

Fields in org.jmlspecs.checker declared as JmlSpecExpression

private JmlSpecExpression	JmlRepresentsDecl.specExpression
private JmlSpecExpression	JmlDurationClause.specExp
protected JmlSpecExpression	JmlSpecExpressionWrapper.specExpression
private JmlSpecExpression[]	JmlFreshExpression.specExpressionList
private JmlSpecExpression	JmlMeasuredClause.specExp
private JmlSpecExpression[]	JmlMonitorsForVarAssertion.specExpressionList
private JmlSpecExpression	JmlName.start
private JmlSpecExpression	JmlName.end
private JmlSpecExpression	JmlPredicate.specExpression
private JmlSpecExpression	JmlSpecQuantifiedExpression.specExpression
private JmlSpecExpression	JmlVariantFunction.specExpression
private JmlSpecExpression	JmlWorkingSpaceClause.specExp

Methods in org.jmlspecs.checker that return JmlSpecExpression

JmlSpecExpression	JmlRepresentsDecl.specExpression() Returns the spec expression of this represents declaration.
JmlSpecExpression	JmlDurationClause.specExp()
JmlSpecExpression	JmlSpecExpressionWrapper.specExpression()
JmlSpecExpression[]	JmlFreshExpression.specExpressionList()
JmlSpecExpression	JmlMeasuredClause.specExp()
JmlSpecExpression[]	JmlMonitorsForVarAssertion.specExpressionList()
JmlSpecExpression	JmlName.start()
JmlSpecExpression	JmlName.end()
JmlSpecExpression	JmlPredicate.specExpression()
JmlSpecExpression	JmlSpecQuantifiedExpression.specExpression()
JmlSpecExpression	JmlVariantFunction.specExpression()
JmlSpecExpression	JmlWorkingSpaceClause.specExp()
JmlSpecExpression	JmlParser.jmlSpecExpression()
JmlSpecExpression[]	JmlParser.jmlSpecExpressionList()
private JmlSpecExpression[]	TestJmlParser.specExpressionListFrom(JmlCompilationUnit unit)

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

void	JmlAbstractVisitor.visitJmlSpecExpression(JmlSpecExpression self)
abstract void	JmlVisitor.visitJmlSpecExpression(JmlSpecExpression self)
void	JmlVisitorNI.visitJmlSpecExpression(JmlSpecExpression self)
void	JmlAccumSubclassingInfo.visitJmlSpecExpression(JmlSpecExpression self)
void	JmlExpressionChecker.visitJmlSpecExpression(JmlSpecExpression self)

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

JmlRepresentsDecl(TokenReference where, long modifiers, boolean redundantly, JmlStoreRefExpression storeRef, JmlSpecExpression specExpression)
Creates a new JmlRepresentsDecl instance.

JmlDurationClause(TokenReference where, boolean isRedundantly, JmlSpecExpression specExp, JmlPredicate pred)

JmlSpecExpressionWrapper(TokenReference where, JmlSpecExpression specExpression)

JmlElemTypeExpression(TokenReference where, JmlSpecExpression specExpression)

JmlFreshExpression(TokenReference where, JmlSpecExpression[] specExpressionList)

JmlInvariantForExpression(TokenReference where, JmlSpecExpression specExpression)

JmlLabelExpression(TokenReference where, boolean isPosLabel, String ident, JmlSpecExpression specExpression)

JmlMeasuredClause(TokenReference where, boolean isRedundantly, JmlSpecExpression specExp, JmlPredicate pred)

JmlMonitorsForVarAssertion(TokenReference where, long modifiers, JNameExpression fieldName, JmlSpecExpression[] specExpressionList)

JmlName(TokenReference where, JmlSpecExpression start)
Construct a [ spec-expression ] sort of store-ref-name-suffix.

JmlName(TokenReference where, JmlSpecExpression start, JmlSpecExpression end)
Construct a an index-range suffix.

JmlNonNullElementsExpression(TokenReference where, JmlSpecExpression specExpression)

JmlOldExpression(TokenReference where, JmlSpecExpression specExpression, String label)

JmlPredicate(JmlSpecExpression specExpression)

JmlPreExpression(TokenReference where, JmlSpecExpression specExpression)

JmlReachExpression(TokenReference where, JmlSpecExpression specExpression, CType referenceType, JmlStoreRefExpression storeRefExpression)

JmlSpaceExpression(TokenReference where, JmlSpecExpression specExpression)

JmlSpecQuantifiedExpression(TokenReference where, int oper, JVariableDefinition[] quantifiedVarDecls, JmlPredicate predicate, JmlSpecExpression specExpression)

JmlTypeOfExpression(TokenReference where, JmlSpecExpression specExpression)

JmlVariantFunction(TokenReference where, boolean isRedundantly, JmlSpecExpression specExpression)

JmlWorkingSpaceClause(TokenReference where, boolean isRedundantly, JmlSpecExpression specExp, JmlPredicate pred)

Uses of JmlSpecExpression in org.jmlspecs.jmldoc.jmldoc_142

Methods in org.jmlspecs.jmldoc.jmldoc_142 with parameters of type JmlSpecExpression

void	SpecWriter.visitJmlSpecExpression(JmlSpecExpression self)

Uses of JmlSpecExpression in org.jmlspecs.jmlrac

Methods in org.jmlspecs.jmlrac with parameters of type JmlSpecExpression

void	RacPrettyPrinter.visitJmlSpecExpression(JmlSpecExpression self) Prints a JML specification expression.
void	TransExpression.visitJmlSpecExpression(JmlSpecExpression self) Translates a JML specification expression.
void	TransExpression2.visitJmlSpecExpression(JmlSpecExpression self) Translates the given JML spec expression.

Constructors in org.jmlspecs.jmlrac with parameters of type JmlSpecExpression

RacPredicate(JmlSpecExpression specExpression)

Uses of JmlSpecExpression in org.jmlspecs.jmlrac.qexpr

Methods in org.jmlspecs.jmlrac.qexpr with parameters of type JmlSpecExpression

void	AbstractExpressionVisitor.visitJmlSpecExpression(JmlSpecExpression self) Visits the given JML spec expression, self.