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

Packages that use JmlMethodSpecification

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

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

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

void	ASTVisitor.endVisit(JmlMethodSpecification jmlMethodSpecification, BlockScope scope)
void	ASTVisitor.endVisit(JmlMethodSpecification jmlMethodSpecification, ClassScope classScope)
boolean	ASTVisitor.visit(JmlMethodSpecification jmlMethodSpecification, BlockScope scope)
boolean	ASTVisitor.visit(JmlMethodSpecification jmlMethodSpecification, ClassScope classScope)

Uses of JmlMethodSpecification in org.jmlspecs.jml4.ast

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

JmlMethodSpecification	JmlMethodDeclaration.specification
JmlMethodSpecification	JmlConstructorDeclaration.specification

Methods in org.jmlspecs.jml4.ast that return JmlMethodSpecification

JmlMethodSpecification	JmlMethodDeclaration.getSpecification()
JmlMethodSpecification	JmlConstructorDeclaration.getSpecification()
JmlMethodSpecification	JmlAbstractMethodDeclaration.getSpecification()

Methods in org.jmlspecs.jml4.ast with parameters of type JmlMethodSpecification

void	JmlMethodDeclaration.setSpecification(JmlMethodSpecification specification)

Uses of JmlMethodSpecification in org.jmlspecs.jml4.fspv

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

void	TraceAstVisitor.endVisit(JmlMethodSpecification jmlMethodSpecification, ClassScope classScope)
boolean	TraceAstVisitor.visit(JmlMethodSpecification jmlMethodSpecification, ClassScope classScope)

Uses of JmlMethodSpecification in org.jmlspecs.jml4.rac

Methods in org.jmlspecs.jml4.rac that return JmlMethodSpecification

static JmlMethodSpecification	RacTranslator.getSpecification(AbstractMethodDeclaration meth) Returns the specification of the given method or constructor.
JmlMethodSpecification	DesugarSpec.perform(JmlMethodSpecification mspec, TypeReference[] exceptions) Returns a desugared specification of the given method specification.

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

void	JmlNullifier.endVisit(JmlMethodSpecification jmlMethodSpecification, BlockScope scope)
void	JmlAstVisitor.endVisit(JmlMethodSpecification jmlMethodSpecification, BlockScope scope)
void	AstDirtyBitsRetriever.endVisit(JmlMethodSpecification jmlMethodSpecification, BlockScope scope)
void	AstDirtyBitsRestorer.endVisit(JmlMethodSpecification jmlMethodSpecification, BlockScope scope)
void	JmlNullifier.endVisit(JmlMethodSpecification jmlMethodSpecification, ClassScope classScope)
void	JmlAstVisitor.endVisit(JmlMethodSpecification jmlMethodSpecification, ClassScope classScope)
void	DefaultRacAstVisitor.endVisit(JmlMethodSpecification jmlMethodSpecification, ClassScope classScope)
void	AstDirtyBitsRetriever.endVisit(JmlMethodSpecification jmlMethodSpecification, ClassScope classScope)
JmlMethodSpecification	DesugarSpec.perform(JmlMethodSpecification mspec, TypeReference[] exceptions) Returns a desugared specification of the given method specification.
MethodDeclaration	PostconditionTranslator.translate(JmlMethodSpecification methSpec, AbstractMethodDeclaration meth, java.util.List<java.lang.String> preVars, VariableGenerator vgen, RacResult result) Translates the postcondition of the given method or constructor and returns a postcondition check method.
MethodDeclaration	ExceptionalPostconditionTranslator.translate(JmlMethodSpecification methSpec, AbstractMethodDeclaration meth, java.util.List<java.lang.String> preVars, VariableGenerator vgen, RacResult result) Translates the exceptional precondition of the given method or constructor and returns an exceptional postcondition check method.
void	PreconditionTranslator.translate(JmlMethodSpecification methSpec, AbstractMethodDeclaration meth, VariableGenerator vgen, RacResult result) Translates the precondition of the given method into RAC code.
void	DesugarSpec.traverse(JmlMethodSpecification self, BlockScope scope)
boolean	JmlNullifier.visit(JmlMethodSpecification jmlMethodSpecification, BlockScope scope)
boolean	JmlAstVisitor.visit(JmlMethodSpecification jmlMethodSpecification, BlockScope scope)
boolean	DesugarSpec.visit(JmlMethodSpecification self, BlockScope scope) Desugars the given JML specification.
boolean	AstDirtyBitsRetriever.visit(JmlMethodSpecification jmlMethodSpecification, BlockScope scope)
boolean	AstDirtyBitsRestorer.visit(JmlMethodSpecification jmlMethodSpecification, BlockScope scope)
boolean	JmlNullifier.visit(JmlMethodSpecification jmlMethodSpecification, ClassScope classScope)
boolean	JmlAstVisitor.visit(JmlMethodSpecification jmlMethodSpecification, ClassScope classScope)
boolean	DefaultRacAstVisitor.visit(JmlMethodSpecification jmlMethodSpecification, ClassScope classScope)
boolean	AstDirtyBitsRetriever.visit(JmlMethodSpecification jmlMethodSpecification, ClassScope classScope)
void	DesugarSpec.visitJmlExtendingSpecification(JmlMethodSpecification self, BlockScope scope) Desugar an extending specification.