Uses of Class
org.jmlspecs.jml4.ast.JmlClause

Packages that use JmlClause

org.eclipse.jdt.internal.compiler
org.jmlspecs.jml4.ast
org.jmlspecs.jml4.fspv
org.jmlspecs.jml4.fspv.phases
org.jmlspecs.jml4.rac

Uses of JmlClause in org.eclipse.jdt.internal.compiler

Methods in org.eclipse.jdt.internal.compiler with parameters of type JmlClause

void	ASTVisitor.endVisit(JmlClause jmlClause, BlockScope scope)
boolean	ASTVisitor.visit(JmlClause jmlClause, BlockScope scope)

Uses of JmlClause in org.jmlspecs.jml4.ast

Subclasses of JmlClause in org.jmlspecs.jml4.ast

class	JmlAssignableClause
class	JmlConstraintClause
class	JmlDivergesClause
class	JmlEnsuresClause
class	JmlInDataGroupClause
class	JmlInitiallyClause
class	JmlInvariantForType
class	JmlLoopInvariant
class	JmlLoopVariant
class	JmlMapsIntoClause
class	JmlRepresentsClause
class	JmlRequiresClause
class	JmlSignalsClause
class	JmlSignalsOnlyClause
class	JmlTypeBodyDeclaration

Fields in org.jmlspecs.jml4.ast declared as JmlClause

JmlClause[]

JmlSpecCaseRestAsClauseSeq.clauses

Constructors in org.jmlspecs.jml4.ast with parameters of type JmlClause

JmlSpecCaseRestAsClauseSeq(JmlClause[] clauses)

Uses of JmlClause in org.jmlspecs.jml4.fspv

Methods in org.jmlspecs.jml4.fspv with parameters of type JmlClause

void	TraceAstVisitor.endVisit(JmlClause jmlClause, BlockScope scope)
void	TheoryTranslator.endVisit(JmlClause jmlClause, BlockScope scope)
boolean	TraceAstVisitor.visit(JmlClause jmlClause, BlockScope scope)
boolean	TheoryTranslator.visit(JmlClause jmlClause, BlockScope scope)

Uses of JmlClause in org.jmlspecs.jml4.fspv.phases

Methods in org.jmlspecs.jml4.fspv.phases with parameters of type JmlClause

void	TheoryTranslation.endVisit(JmlClause jmlClause, BlockScope scope)
boolean	TheoryTranslation.visit(JmlClause jmlClause, BlockScope scope)

Uses of JmlClause in org.jmlspecs.jml4.rac

Methods in org.jmlspecs.jml4.rac with parameters of type JmlClause

void	JmlAstVisitor.endVisit(JmlClause jmlClause, BlockScope scope)
void	DefaultRacAstVisitor.endVisit(JmlClause jmlClause, BlockScope scope)
void	AstDirtyBitsRetriever.endVisit(JmlClause jmlClause, BlockScope scope)
void	AstDirtyBitsRestorer.endVisit(JmlClause jmlClause, BlockScope scope)
boolean	JmlAstVisitor.visit(JmlClause jmlClause, BlockScope scope)
boolean	DefaultRacAstVisitor.visit(JmlClause jmlClause, BlockScope scope)
boolean	AstDirtyBitsRetriever.visit(JmlClause jmlClause, BlockScope scope)
boolean	AstDirtyBitsRestorer.visit(JmlClause jmlClause, BlockScope scope)