Uses of Class
org.jmlspecs.checker.JmlNode

Packages that use JmlNode

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 JmlNode in org.jmlspecs.checker

Subclasses of JmlNode in org.jmlspecs.checker

class	JmlAbruptSpecBody JmlAbruptSpecBody.java
class	JmlAbruptSpecCase JmlAbruptSpecCase.java
class	JmlAccessibleClause An AST node class representing the JML accessible clause.
class	JmlAssignableClause A JML AST node for the assignable clause.
class	JmlAxiom This AST node represents a JML axiom annotation.
class	JmlBehaviorSpec JmlBehaviorSpec.java heavyweight-spec ::= [ privacy ] "behavior" generic-spec-case
class	JmlBinaryField This class represents a class read from a *.class file.
class	JmlBinaryMember This type represents a java declaration in the syntax tree.
class	JmlBinaryMethod This class represents a method read from a *.class file.
class	JmlBinaryType This class represents a class read from a *.class file.
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	JmlClassDeclaration This type represents a java class declaration in the syntax tree.
class	JmlClassOrGFImport This type represents (in the AST) import statements for single classes or generic functions, e.g., import java.util.ArrayList; or import org.multijava.samples.typecheck.
class	JmlCodeContract An abstraction of JML method specification.
class	JmlCompilationUnit This class represents a single JML compilation unit (typically a file in a file-based compiler like this) in the AST.
class	JmlConstraint This AST node represents a JML constraint annotation.
class	JmlConstructorDeclaration JmlConstructorDeclaration.java
class	JmlConstructorName This AST node represents a constructor in a JML annotation.
class	JmlContinuesClause JmlContinuesClause.java
class	JmlDataGroupClause This class represents a jml-var-assertion of the form initially predicate.
class	JmlDeclaration This abstract class is the superclass of all jml-declaration AST nodes, (i.e., invariants, history constraints, depends declarations, and represents declarations)
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	JmlExample A class representing JML example specifications.
class	JmlExceptionalBehaviorSpec JmlExceptionalBehaviorSpec.java heavyweight-spec ::= [ privacy ] "exceptional_behavior" exceptional-spec-case
class	JmlExceptionalExample A class representing JML exceptional example specifications.
class	JmlExceptionalSpecBody An AST node class for the JML exceptional-spec-body.
class	JmlExceptionalSpecCase An AST node class for the JML exceptional-spec-case.
class	JmlExtendingSpecification A method specification that extetends inherited specifications.
class	JmlFieldDeclaration JmlFieldDeclaration.java
class	JmlForAllVarDecl An AST node class for the JML forall variable declarations.
class	JmlGeneralSpecCase An abstraction of JML specification cases.
class	JmlGenericSpecBody An AST node class for the JML generic-spec-body.
class	JmlGenericSpecCase An AST node class for the JML generic-spec-case.
class	JmlHeavyweightSpec An AST node class for the JML heavyweight-spec.
class	JmlInformalStoreRef JmlInformalStoreRef.java
class	JmlInGroupClause This class represents a jml-var-assertion of the form initially predicate.
class	JmlInitiallyVarAssertion This class represents a jml-var-assertion of the form initially predicate.
class	JmlInterfaceDeclaration This class represents a java interface in the syntax tree
class	JmlInvariant This AST node represents a JML invariant annotation.
class	JmlLabeled JmlLabeledClause.java
class	JmlLetVarDecl An AST node class for the JML let (old) variable declarations.
class	JmlLoopInvariant JmlLoopInvariant.java
class	JmlLoopSpecification This is the super class for the classes representing loop-invariant and variant-function annotations for loop-stmt.
class	JmlMapsIntoClause This class represents a jml-var-assertion of the form initially predicate.
class	JmlMeasuredClause JmlMeasuredClause.java
class	JmlMemberDeclaration This type represents a java declaration in the syntax tree.
class	JmlMethodDeclaration JmlMethodDeclaration.java
class	JmlMethodName This AST node represents a method name in a JML annotation.
class	JmlMethodSpecification An abstraction of JML method specification.
class	JmlModelProgram JmlModelProgram.java
class	JmlMonitorsForVarAssertion JmlMonitorsForVarAssertion.java
class	JmlName This class represents a store-ref-name, store-ref-name-suffix, method-res-start, or identifier from a method-ref in an AST.
class	JmlNormalBehaviorSpec JmlNormalBehaviorSpec.java heavyweight-spec ::= [ privacy ] "normal_behavior" normal-spec-case
class	JmlNormalExample A class representing JML normal example specifications.
class	JmlNormalSpecBody An AST node class for the JML normal-spec-body.
class	JmlNormalSpecCase An AST node class for the JML normal-spec-case.
class	JmlPackageImport This type represents (in the AST) full-package import statements.
class	JmlPredicateClause JmlPredicateClause.java
class	JmlReadableIfVarAssertion This class represents a jml-var-assertion of the form readable id if predicate.
class	JmlRedundantSpec A class representing JML redundant specifications.
class	JmlRefinePrefix
class	JmlRepresentsDecl This AST node represents a JML represents declaration annotation.
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	JmlSpecBody JmlSpecBodyClause.java
class	JmlSpecBodyClause This abstract class is the common superclass of different kinds of specification clauses appearing in the specification body such as JmlAccessibleClause, JmlAssignableClause, JmlCallableClause, and JmlPredicateClause.
class	JmlSpecCase An abstraction of JML specification cases.
class	JmlSpecification JmlSpecification.java
class	JmlSpecStatementClause JmlSpecStatementClause.java
class	JmlSpecVarDecl An abstraction of JML specification variable declarations.
class	JmlStoreRef An abstraction of JML store references.
class	JmlStoreRefExpression An AST node class for JML store reference expressions.
class	JmlStoreRefKeyword This class represents a JmlStoreRefKeyword in the AST.
class	JmlTypeDeclaration This type represents a java class or interface in the syntax tree.
class	JmlVarAssertion This class represents jml-var-assertion in JML ASTs.
class	JmlVariantFunction JmlVariantFunction.java
class	JmlWhenClause JmlWhenClause.java
class	JmlWorkingSpaceClause JmlWorkingSpaceClause.java
class	JmlWritableIfVarAssertion This class represents a jml-var-assertion of the form writable id if predicate.

Methods in org.jmlspecs.checker that return JmlNode

abstract JmlNode[]

JmlAnnotatable.jmlAnnotations() Returns an array of the JML annotations for this AST node.

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

void	JmlAbstractVisitor.visitJmlNode(JmlNode self)
abstract void	JmlVisitor.visitJmlNode(JmlNode self)
void	JmlVisitorNI.visitJmlNode(JmlNode self)

Uses of JmlNode in org.jmlspecs.jmldoc.jmldoc_142

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

void	SpecWriter.visitJmlNode(JmlNode self)

Uses of JmlNode in org.jmlspecs.jmlrac

Subclasses of JmlNode in org.jmlspecs.jmlrac

static class

RacParser.RacMethodDeclaration A RAC node class for representing method declarations.

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

void	RacPrettyPrinter.visitJmlNode(JmlNode self)