Uses of Class
org.jmlspecs.checker.JmlSpecBodyClause

Packages that use JmlSpecBodyClause

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.

Uses of JmlSpecBodyClause in org.jmlspecs.checker

Subclasses of JmlSpecBodyClause in org.jmlspecs.checker

class	JmlAccessibleClause An AST node class representing the JML accessible clause.
class	JmlAssignableClause A JML AST node for the assignable clause.
class	JmlBreaksClause JmlBreaksClause.java
class	JmlCallableClause An AST node class representing the JML callable clause.
class	JmlCapturesClause An AST node class representing the JML captures clause.
class	JmlContinuesClause JmlContinuesClause.java
class	JmlDivergesClause A JML AST node class for the diverges clause.
class	JmlDurationClause JmlDurationClause.java
class	JmlEnsuresClause A JML AST node for the <\code>ensures clause.
class	JmlLabeled JmlLabeledClause.java
class	JmlMeasuredClause JmlMeasuredClause.java
class	JmlPredicateClause JmlPredicateClause.java
class	JmlRequiresClause JmlRequiresClause.java
class	JmlReturnsClause JmlReturnsClause.java
class	JmlSignalsClause A JML AST node class for the signals clause.
class	JmlSignalsOnlyClause A JML AST node class for the signals_only clause.
class	JmlSpecStatementClause JmlSpecStatementClause.java
class	JmlWhenClause JmlWhenClause.java
class	JmlWorkingSpaceClause JmlWorkingSpaceClause.java

Fields in org.jmlspecs.checker declared as JmlSpecBodyClause

protected JmlSpecBodyClause[]	JmlSpecBody.specClauses
private JmlSpecBodyClause[]	JmlExample.specBody

Methods in org.jmlspecs.checker that return JmlSpecBodyClause

JmlSpecBodyClause[]	JmlSpecBody.specClauses()
JmlSpecBodyClause[]	JmlExample.specClauses() Deprecated
JmlSpecBodyClause[]	JmlExample.specBody()
JmlSpecBodyClause[]	JmlGenericSpecBody.simpleSpecBodies()
JmlSpecBodyClause[]	JmlParser.jmlSpecBody()
JmlSpecBodyClause	JmlParser.jmlSpecBodyClause()
protected JmlSpecBodyClause[]	TestJmlParser.Helper.getSpecBody(String sourceCode)
protected JmlSpecBodyClause	TestJmlParser.Helper.getSpecBodyClause(String sourceCode)

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

boolean	JmlParser.verifySimpleSpecBody(JmlSpecBodyClause[] clauses) Returns true if all elements of the argument are simple spec body clauses; otherwise, print an appropriate error message and return false
boolean	JmlParser.verifyNormalSpecBody(JmlSpecBodyClause[] clauses) Returns true if all elements of the argument are normal spec body clauses; otherwise, print an appropriate error message and return false
boolean	JmlParser.verifyExceptionalSpecBody(JmlSpecBodyClause[] clauses) Returns true if all elements of the argument are exceptional spec body clauses; otherwise, print an appropriate error message and return false
boolean	JmlParser.verifySimpleSpecStatementBody(JmlSpecBodyClause[] clauses) Returns true if all elements of the argument are simple spec statement body clauses; otherwise, print an appropriate error message and return false
boolean	JmlParser.verifyAbruptSpecBody(JmlSpecBodyClause[] clauses) Returns true if all elements of the argument are abrupt spec body clauses; otherwise, print an appropriate error message and return false
static void	NonNullStatistics.checkSpecBodyClause(JmlSpecBodyClause jsbc, JmlContext context, String fn)
private JmlStoreRef	TestJmlParser.storeRefFromCC(JmlSpecBodyClause bc)
private JmlStoreRef	TestJmlParser.storeRefFrom(JmlSpecBodyClause bc)

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

JmlSpecBody(JmlSpecBodyClause[] specClauses)

JmlAbruptSpecBody(JmlSpecBodyClause[] specClauses)

JmlExample(TokenReference where, long privacy, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlSpecBodyClause[] specBody)
Constructs a new instance with given arguments.

JmlExample(TokenReference where, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlSpecBodyClause[] specBody)
Constructs a new instance with given arguments.

JmlExceptionalExample(TokenReference where, long privacy, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlSpecBodyClause[] specClauses)
Constructs a new instance with given arguments.

JmlExceptionalSpecBody(JmlSpecBodyClause[] specClauses)

JmlGenericSpecBody(JmlSpecBodyClause[] specClauses)

JmlNormalExample(TokenReference where, long privacy, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlSpecBodyClause[] specClauses)
Constructs a new instance with given arguments.

JmlNormalSpecBody(JmlSpecBodyClause[] specClauses)

Uses of JmlSpecBodyClause in org.jmlspecs.jmldoc.jmldoc_142

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

void	SpecWriter.visitJmlSpecBodyClause(JmlSpecBodyClause self)

Uses of JmlSpecBodyClause in org.jmlspecs.jmlrac

Fields in org.jmlspecs.jmlrac declared as JmlSpecBodyClause

protected JmlSpecBodyClause[]

TransMethod.SpecCase.bodyClauses

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

private void	DesugarSpec.visitSpecBody(JmlSpecBody self, JmlSpecBodyClause body) Desugars a specification body (general, normal, exceptional).
protected boolean	TransMethod.SpecCase.isCheckable(JmlSpecBodyClause clause) Returns true if the given spec body clause is checkable.

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

TransMethod.SpecCase(JmlSpecBodyClause[] bc)