org.checkerframework.framework.util

Class FieldInvariants

java.lang.Object

org.checkerframework.framework.util.FieldInvariants

public class FieldInvariants
extends java.lang.Object

Represents field invariants, which the user states by writing @FieldInvariant. Think of this as a set of (field, qualifier) pairs.

A FieldInvariants object may be malformed (inconsistent number of fields and qualifiers). In this case, the BaseTypeVisitor will issue an error.

Constructor Summary

Constructors

Constructor and Description
FieldInvariants(FieldInvariants other, java.util.List<java.lang.String> fields, java.util.List<javax.lang.model.element.AnnotationMirror> qualifiers) Creates a new object with all the invariants in other, plus those specified by fields and qualifiers.
FieldInvariants(java.util.List<java.lang.String> fields, java.util.List<javax.lang.model.element.AnnotationMirror> qualifiers) Creates a new FieldInvariants object.

Method Summary

Modifier and Type	Method and Description
java.util.List<java.lang.String>	getFields() The simple names of the fields that have a qualifier.
java.util.List<javax.lang.model.element.AnnotationMirror>	getQualifiersFor(java.lang.CharSequence field) Returns a list of qualifiers for field.
Result	isSuperInvariant(FieldInvariants superInvar, AnnotatedTypeFactory factory)
boolean	isWellFormed()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

FieldInvariants

public FieldInvariants(java.util.List<java.lang.String> fields,
                       java.util.List<javax.lang.model.element.AnnotationMirror> qualifiers)

Creates a new FieldInvariants object. The result is well-formed if length of qualifiers is either 1 or equal to length of fields.

Parameters:

fields - list of fields

qualifiers - list of qualifiers

FieldInvariants

public FieldInvariants(FieldInvariants other,
                       java.util.List<java.lang.String> fields,
                       java.util.List<javax.lang.model.element.AnnotationMirror> qualifiers)

Creates a new object with all the invariants in other, plus those specified by fields and qualifiers. The result is well-formed if length of qualifiers is either 1 or equal to length of fields.

Parameters:

other - other invariant object, may be null

fields - list of fields

qualifiers - list of qualifiers

Method Detail

getFields

public java.util.List<java.lang.String> getFields()

The simple names of the fields that have a qualifier. May contain duplicates.

getQualifiersFor

public java.util.List<javax.lang.model.element.AnnotationMirror> getQualifiersFor(java.lang.CharSequence field)

Returns a list of qualifiers for field. If field has no qualifiers, returns an empty list.

Parameters:

field - simple field name

Returns:

a list of qualifiers for field, possibly empty

isWellFormed

public boolean isWellFormed()

Returns:

true if there is a qualifier for each field in fields

isSuperInvariant

public Result isSuperInvariant(FieldInvariants superInvar,
                               AnnotatedTypeFactory factory)

Returns:

null if superInvar is a super invariant, otherwise returns a Result with the error message