Uses of Class
org.jmlspecs.checker.JmlSourceMethod

Packages that use JmlSourceMethod

org.jmlspecs.checker

Contains the source code for a parser and typechecker for JML annotations and java code.

Uses of JmlSourceMethod in org.jmlspecs.checker

Methods in org.jmlspecs.checker that return JmlSourceMethod

JmlSourceMethod	JmlSourceClass.lookupRefinedMethod(CMethod specMethod) Searches for the method refined by a given method, looking in the refinement hierarchy as needed.
JmlSourceMethod	JmlSourceMethod.getMostRefined() Returns the most refined declaration AST for this method.

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

JmlAssignableFieldSet	JmlSpecBody.getAssignableFieldSet(JmlSourceMethod method) Returns the maximal set of fields that can be assigned to by the given method (takes the union of the assignable clauses from all specification cases).
JmlAssignableFieldSet	JmlSpecBody.getMinAssignableFieldSet(JmlSourceMethod method, JmlDataGroupMemberMap dataGroupMap) Returns the minimal set of fields that can be assigned to by the given method (takes the intersection of the assignable clauses of all specification cases).
abstract JmlAssignableFieldSet	JmlSpecCase.getAssignableFieldSet(JmlSourceMethod method) Returns the maximal set of fields that can be assigned to by this method (takes the union of the assignable clauses from all specification cases).
JmlAssignableFieldSet	JmlGeneralSpecCase.getAssignableFieldSet(JmlSourceMethod method) Returns the maximal set of fields that can be assigned to by the given method (takes the union of the assignable clauses from all specification cases).
JmlAssignableFieldSet	JmlGeneralSpecCase.getMinAssignableFieldSet(JmlSourceMethod method, JmlDataGroupMemberMap dataGroupMap) Returns the minimal set of fields that can be assigned to by the given method (takes the intersection of the assignable clauses of all specification cases).
JmlAssignableFieldSet	JmlAssignableClause.getAssignableFieldSet(JmlSourceMethod method)
JmlAssignableFieldSet	JmlHeavyweightSpec.getAssignableFieldSet(JmlSourceMethod method) Returns the maximal set of fields that can be assigned to by the given method (takes the union of the assignable clauses from all specification cases).
JmlAssignableFieldSet	JmlCodeContract.getAssignableFieldSet(JmlSourceMethod method) Returns an empty set since there are no assignable clauses in the "code_contract".
private void	JmlMethodDeclaration.checkNullityForOverriddenMethods(CContextType context, JmlSourceMethod self)
private void	JmlMethodDeclaration.checkParamNullity(CContextType context, JmlSourceMethod self, JmlSourceMethod overriddenMeth) Ensure that nullity modifiers of the parameter(s) of self exactly match with the corresponding parameter(s) of overriddenMeth, a method that it overrides.
private void	JmlMethodDeclaration.checkResultNullity(CContextType context, JmlSourceMethod self, JmlSourceMethod overriddenMeth) Ensure that nullity modifiers of the (return type of) self are consistent with overriddenMeth, a method that it overrides.
private void	JmlMethodDeclaration.checkMethodSpecification(CClassContextType cContext, JmlSourceMethod self)
void	JmlMethodDeclaration.jmlchecks(CContextType context, JmlSourceMethod self)
abstract JmlAssignableFieldSet	JmlMethodSpecification.getAssignableFieldSet(JmlSourceMethod method) Returns the maximal set of fields that can be assigned to by the given method (takes the union of the assignable clauses from all specification cases).
abstract JmlAssignableFieldSet	JmlMethodSpecification.getMinAssignableFieldSet(JmlSourceMethod method, JmlDataGroupMemberMap dataGroupMap) Returns the minimal set of fields that can be assigned to by the given method (takes the intersection of the assignable clauses of all specification cases).
JmlAssignableFieldSet	JmlSpecification.getAssignableFieldSet(JmlSourceMethod method) Returns the maximal set of fields that can be assigned to by the given method (takes the union of the assignable clauses from all specification cases).
JmlAssignableFieldSet	JmlSpecification.getMinAssignableFieldSet(JmlSourceMethod method, JmlDataGroupMemberMap dataGroupMap) Returns the minimal set of fields that can be assigned to by the given method (takes the intersection of the assignable clauses of all specification cases).
JmlAssignableFieldSet	JmlModelProgram.getAssignableFieldSet(JmlSourceMethod method) Returns the maximal set of fields that can be assigned to by this method (takes the union of the assignable clauses from all specification cases).
static boolean	NonNullStatistics.getSuperMethod(JmlSourceMethod sm)
static boolean	NonNullStatistics.getSuperParam(JmlSourceMethod sm, int i)

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

JmlBinaryMethod(TokenReference where, JmlSourceMethod member)
Constructs a class export from file.