Uses of Class
org.jmlspecs.checker.JmlDataGroupMemberMap

Packages that use JmlDataGroupMemberMap

org.jmlspecs.checker

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

Uses of JmlDataGroupMemberMap in org.jmlspecs.checker

Fields in org.jmlspecs.checker declared as JmlDataGroupMemberMap

protected JmlDataGroupMemberMap

JmlTypeDeclaration.dataGroupMap

Methods in org.jmlspecs.checker that return JmlDataGroupMemberMap

JmlDataGroupMemberMap

JmlTypeDeclaration.getDataGroupMap() Computes the data group map (if it has not already been computed) and returns it.

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

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).
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	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).
void	JmlMethodDeclaration.checkAssignableFields(JmlDataGroupMemberMap dataGroupMap)
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.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).
void	JmlFieldDeclaration.addToDataGroups(JmlDataGroupMemberMap dataGroupMap)
void	JmlFieldDeclaration.addSelfToInDataGroups(JmlSourceField self, JmlInGroupClause inGroupClause, JmlDataGroupMemberMap dataGroupMap)
boolean	JmlAssignableFieldSet.contains(CField field, JmlDataGroupMemberMap dgMap)
boolean	JmlAssignableFieldSet.contains(JClassFieldExpression fieldExpr, JmlDataGroupMemberMap dgMap)
boolean	JmlAssignableFieldSet.isSubsetOf(JmlAssignableFieldSet otherSet, JmlDataGroupMemberMap dgMap)
boolean	JmlAssignableFieldSet.isSupersetOf(JmlAssignableFieldSet otherSet, JmlDataGroupMemberMap dgMap)
JmlAssignableFieldSet	JmlAssignableFieldSet.intersect(JmlAssignableFieldSet otherSet, JmlDataGroupMemberMap dgMap)
void	JmlDataGroupMemberMap.addInheritedMembers(JmlDataGroupMemberMap parentMap) Add mappings for any groups in parentMap that are already in this map.