Package org.checkerframework.framework.util

Class FieldInvariants

java.lang.Object
org.checkerframework.framework.util.FieldInvariants
public class FieldInvariants extends Object
Represents field invariants, which the user states by writing @FieldInvariant. Think of this as a set of (field name, qualifier) pairs.

If a FieldInvariants object is malformed (inconsistent number of fields and qualifiers), BaseTypeVisitor will issue an error.

  • Constructor Details

    • FieldInvariants

      public FieldInvariants(List<String> fields, List<AnnotationMirror> qualifiers, AnnotatedTypeFactory factory)
      Creates a new FieldInvariants object. The result is well-formed if the length of qualifiers is either 1 or equal to length of fields.
      Parameters:
      fields - list of fields
      qualifiers - list of qualifiers, or a single qualifier that applies to all fields
      factory - the type factory

    • FieldInvariants

      public FieldInvariants(FieldInvariants other, List<String> fields, List<AnnotationMirror> qualifiers, AnnotatedTypeFactory factory)
      Creates a new object with all the invariants in other, plus those specified by fields and qualifiers. The result is well-formed if the 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
      factory - the type factory

  • Method Details

    • getFields

      public List<String> getFields()
      The simple names of the fields that have a qualifier. May contain duplicates.

    • getQualifiersFor

      public List<AnnotationMirror> getQualifiersFor(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.
      Returns:
      true if there is a qualifier for each field in fields

    • isStrongerThan

      public @Nullable DiagMessage isStrongerThan(FieldInvariants superInvar)
      Returns null if this is stronger than the given FieldInvariants, otherwise returns the error message. This is stronger if each of its qualifiers is a subtype of (or equal to) the respective qualfier in the given FieldInvariants.
      Parameters:
      superInvar - the value to check for being a weaker invariant
      Returns:
      null if this is stronger, otherwise returns an error message