Uses of Class
org.jmlspecs.checker.JmlAssignableFieldSet

Packages that use JmlAssignableFieldSet

org.jmlspecs.checker

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

Uses of JmlAssignableFieldSet in org.jmlspecs.checker

Fields in org.jmlspecs.checker declared as JmlAssignableFieldSet

protected JmlAssignableFieldSet	JmlSpecBody.assignableFieldSet
protected JmlAssignableFieldSet	JmlSpecBody.minAssignableFieldSet
protected JmlAssignableFieldSet	JmlGeneralSpecCase.assignableFieldSet
protected JmlAssignableFieldSet	JmlGeneralSpecCase.minAssignableFieldSet
private JmlAssignableFieldSet	JmlAssignableClause.fieldSet
private JmlAssignableFieldSet	JmlMethodDeclaration.assignableFieldSet
private JmlAssignableFieldSet	JmlMethodDeclaration.minAssignableFieldSet
protected JmlAssignableFieldSet	JmlSpecification.assignableFieldSet
protected JmlAssignableFieldSet	JmlSpecification.minAssignableFieldSet
protected JmlAssignableFieldSet	JmlModelProgram.assignableFieldSet

Methods in org.jmlspecs.checker that return JmlAssignableFieldSet

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	JmlAssignableClause.getAssignableFieldSet()
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".
JmlAssignableFieldSet	JmlMethodDeclaration.getAssignableFieldSet() 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	JmlMethodDeclaration.getMinAssignableFieldSet(JmlDataGroupMemberMap dataGroupMap) Returns the minimal set of fields that can be assigned to by this method (takes the intersection of the assignable clauses from the specification cases).
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).
JmlAssignableFieldSet	JmlAssignableFieldSet.intersect(JmlAssignableFieldSet otherSet, JmlDataGroupMemberMap dgMap)
JmlAssignableFieldSet	JmlDataGroupMemberMap.getMembers(JmlSourceField group) Returns the members of the given data group.

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

boolean	JmlAssignableFieldSet.addAll(JmlAssignableFieldSet otherSet)
boolean	JmlAssignableFieldSet.isSubsetOf(JmlAssignableFieldSet otherSet, JmlDataGroupMemberMap dgMap)
boolean	JmlAssignableFieldSet.isSupersetOf(JmlAssignableFieldSet otherSet, JmlDataGroupMemberMap dgMap)
JmlAssignableFieldSet	JmlAssignableFieldSet.intersect(JmlAssignableFieldSet otherSet, JmlDataGroupMemberMap dgMap)
void	JmlDataGroupMemberMap.addMembers(JmlSourceField group, JmlAssignableFieldSet members) Add a mapping for group if it is not already in this map.

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

JmlAssignableFieldSet(JmlAssignableFieldSet other)