Uses of Package
org.jmlspecs.jml4.ast

Packages that use org.jmlspecs.jml4.ast

org.eclipse.jdt.internal.compiler
org.eclipse.jdt.internal.compiler.problem
org.jmlspecs.eclipse.jdt.internal.esc2
org.jmlspecs.jml4.ast
org.jmlspecs.jml4.esc
org.jmlspecs.jml4.esc.gc
org.jmlspecs.jml4.fspv
org.jmlspecs.jml4.fspv.phases
org.jmlspecs.jml4.rac
org.jmlspecs.jml4.rac.quantifiedexpression
org.jmlspecs.jml4.util

Classes in org.jmlspecs.jml4.ast used by org.eclipse.jdt.internal.compiler

JmlArrayQualifiedTypeReference

JmlArrayReference

JmlArrayTypeReference

JmlAssertStatement

JmlAssignment

JmlAssumeStatement

JmlBooleanQuantifier

JmlCastExpression

JmlCastExpressionWithoutType

JmlClause
An abstraction of a JML clause which can be either a: - type body clause, - method spec clause, - statement body clause.

JmlCompilationUnitDeclaration

JmlConstructorDeclaration

JmlDoStatement

JmlElemtypeExpression

JmlEnsuresClause

JmlExplicitConstructorCall

JmlFieldDeclaration

JmlFieldReference

JmlForeachStatement

JmlForStatement

JmlFreshExpression

JmlGroupName
Deprecated.

JmlLocalDeclaration

JmlLoopAnnotations

JmlLoopInvariant

JmlLoopVariant

JmlMapsIntoClause

JmlMapsMemberRefExpr
Deprecated.

JmlMemberFieldRef
Deprecated.

JmlMessageSend

JmlMethodDeclaration

JmlMethodSpecification

JmlModifier
This class offers services for processing JML modifiers.

JmlName

JmlNumericQuantifier

JmlOldExpression

JmlParameterizedQualifiedTypeReference

JmlParameterizedSingleTypeReference

JmlQualifiedNameReference

JmlQualifiedTypeReference

JmlQuantifiedExpression

JmlRequiresClause

JmlResultReference

JmlReturnStatement

JmlSetComprehension

JmlSetStatement

JmlSingleNameReference

JmlSingleTypeReference

JmlSpecCase

JmlSpecCaseBlock

JmlSpecCaseBody

JmlSpecCaseHeader

JmlSpecCaseRestAsClauseSeq

JmlStoreRefExpression
Deprecated.

JmlSubtypeExpression

JmlTypeDeclaration

JmlTypeExpression

JmlTypeofExpression

JmlWhileStatement

JmlWildcard

Classes in org.jmlspecs.jml4.ast used by org.eclipse.jdt.internal.compiler.problem

JmlMethodDeclaration

JmlTypeBodyDeclaration

Classes in org.jmlspecs.jml4.ast used by org.jmlspecs.eclipse.jdt.internal.esc2

JmlArrayQualifiedTypeReference

JmlArrayReference

JmlArrayTypeReference

JmlAssertStatement

JmlAssignment

JmlCastExpression

JmlCastExpressionWithoutType

JmlCompilationUnitDeclaration

JmlConstructorDeclaration

JmlEnsuresClause

JmlFieldDeclaration

JmlFieldReference

JmlLocalDeclaration

JmlMessageSend

JmlMethodDeclaration

JmlParameterizedQualifiedTypeReference

JmlParameterizedSingleTypeReference

JmlQualifiedNameReference

JmlQualifiedTypeReference

JmlRequiresClause

JmlResultReference

JmlReturnStatement

JmlSingleNameReference

JmlSingleTypeReference

JmlWildcard

Classes in org.jmlspecs.jml4.ast used by org.jmlspecs.jml4.ast

JmlAbstractMethodDeclaration

JmlAllRangeExpression

JmlArrayIndexRangeExpression

JmlArrayReference

JmlAssertOrAssumeStatement

JmlAssignment

JmlCastExpression

JmlClause
An abstraction of a JML clause which can be either a: - type body clause, - method spec clause, - statement body clause.

JmlConstraintClause

JmlDataGroupClause

JmlInitiallyClause

JmlInvariantForType

JmlKeywordExpression
Instances of this class represent various JML keywords that are used in contexts where expressions (predicates or store references) are expected.

JmlLocalDeclaration

JmlLoopAnnotations

JmlLoopInvariant

JmlLoopVariant

JmlMapsMemberRefExpr
Deprecated.

JmlMethodSpecification

JmlMultiReferenceExpression

JmlName

JmlQuantifier

JmlRepresentsClause

JmlRequiresClause

JmlSpecCase

JmlSpecCaseBody

JmlSpecCaseHeader

JmlSpecCaseRest

JmlStoreRefListExpression

JmlTypeBodyDeclaration

JmlTypeReference

JmlUnaryExpression
NOTE: operators taking a list of store ref, like \not_modified() are modeled as unary operators -- taking a single argument consisting of the entire list.

Classes in org.jmlspecs.jml4.ast used by org.jmlspecs.jml4.esc

JmlAbstractMethodDeclaration

JmlTypeDeclaration

Classes in org.jmlspecs.jml4.ast used by org.jmlspecs.jml4.esc.gc

JmlAbstractMethodDeclaration

JmlAssertStatement

JmlAssumeStatement

JmlLoopInvariant

JmlLoopVariant

JmlQuantifiedExpression

JmlResultReference

JmlWhileStatement

Classes in org.jmlspecs.jml4.ast used by org.jmlspecs.jml4.fspv

JmlArrayQualifiedTypeReference

JmlArrayReference

JmlArrayTypeReference

JmlAssertStatement

JmlAssignment

JmlAssumeStatement

JmlCastExpression

JmlCastExpressionWithoutType

JmlClause
An abstraction of a JML clause which can be either a: - type body clause, - method spec clause, - statement body clause.

JmlCompilationUnitDeclaration

JmlConstructorDeclaration

JmlEnsuresClause

JmlFieldDeclaration

JmlFieldReference

JmlLocalDeclaration

JmlLoopAnnotations

JmlLoopInvariant

JmlLoopVariant

JmlMessageSend

JmlMethodDeclaration

JmlMethodSpecification

JmlOldExpression

JmlParameterizedQualifiedTypeReference

JmlParameterizedSingleTypeReference

JmlQualifiedNameReference

JmlQualifiedTypeReference

JmlQuantifiedExpression

JmlRequiresClause

JmlResultReference

JmlReturnStatement

JmlSingleNameReference

JmlSingleTypeReference

JmlWhileStatement

JmlWildcard

Classes in org.jmlspecs.jml4.ast used by org.jmlspecs.jml4.fspv.phases

JmlAssignment

JmlClause
An abstraction of a JML clause which can be either a: - type body clause, - method spec clause, - statement body clause.

JmlCompilationUnitDeclaration

JmlConstructorDeclaration

JmlLoopAnnotations

JmlLoopInvariant

JmlLoopVariant

JmlMethodDeclaration

JmlOldExpression

JmlResultReference

JmlWhileStatement

Classes in org.jmlspecs.jml4.ast used by org.jmlspecs.jml4.rac

JmlAbstractMethodDeclaration

JmlAllocationExpression

JmlArrayQualifiedTypeReference

JmlArrayReference

JmlArrayTypeReference

JmlAssertOrAssumeStatement

JmlAssertStatement

JmlAssignableClause

JmlAssignment

JmlAssumeStatement

JmlBooleanQuantifier

JmlCastExpression

JmlCastExpressionWithoutType

JmlClause
An abstraction of a JML clause which can be either a: - type body clause, - method spec clause, - statement body clause.

JmlClinit

JmlCompilationUnitDeclaration

JmlConditionalExpression

JmlConstraintClause

JmlConstructorDeclaration

JmlDoStatement

JmlElemtypeExpression

JmlEnsuresClause

JmlExplicitConstructorCall

JmlFieldDeclaration

JmlFieldReference

JmlForeachStatement

JmlForStatement

JmlFreshExpression

JmlGroupName
Deprecated.

JmlInitiallyClause

JmlInvariantForType

JmlLocalDeclaration

JmlLoopAnnotations

JmlLoopInvariant

JmlLoopVariant

JmlMapsIntoClause

JmlMapsMemberRefExpr
Deprecated.

JmlMemberFieldRef
Deprecated.

JmlMessageSend

JmlMethodDeclaration

JmlMethodSpecification

JmlModifier
This class offers services for processing JML modifiers.

JmlName

JmlNumericQuantifier

JmlOldExpression

JmlParameterizedQualifiedTypeReference

JmlParameterizedSingleTypeReference

JmlQualifiedNameReference

JmlQualifiedTypeReference

JmlQuantifiedExpression

JmlRepresentsClause

JmlRequiresClause

JmlResultReference

JmlReturnStatement

JmlSetComprehension

JmlSetStatement

JmlSignalsClause

JmlSignalsOnlyClause

JmlSingleNameReference

JmlSingleTypeReference

JmlSpecCase

JmlSpecCaseBlock

JmlSpecCaseBody

JmlSpecCaseHeader

JmlSpecCaseRest

JmlSpecCaseRestAsClauseSeq

JmlStoreRefExpression
Deprecated.

JmlSubtypeExpression

JmlTypeBodyDeclaration

JmlTypeDeclaration

JmlTypeExpression

JmlTypeofExpression

JmlUnaryExpression
NOTE: operators taking a list of store ref, like \not_modified() are modeled as unary operators -- taking a single argument consisting of the entire list.

JmlWhileStatement

JmlWildcard

Classes in org.jmlspecs.jml4.ast used by org.jmlspecs.jml4.rac.quantifiedexpression

JmlQuantifiedExpression

Classes in org.jmlspecs.jml4.ast used by org.jmlspecs.jml4.util

JmlAssignment