Package daikon

Class AnnotateNullable

  • public class AnnotateNullable
extends Object
    AnnotateNullable reads a Daikon invariant file and determines which reference variables have seen any null values. It writes to standard out an annotation file with those variables. It determines which variables have seen null values by looking at the NonZero invariant. If that invariant is NOT present, then the variable must have been null at least once.

    Since only the NonZero invariant is used, Daikon processing time can be significantly reduced by turning off derived variables and all invariants other than daikon.inv.unary.scalar.NonZero. This is not necessary, however, for correct operation. File annotate_nullable.config in the distribution does this.

    • Field Detail

      • stub_format

        public static boolean stub_format
        Write an output file in the stub class format (see the Checker Framework Manual), instead of in annotation file format.

      • nonnull_annotations

        public static boolean nonnull_annotations
        Adds NonNull annotations as well as Nullable annotations. Unlike Nullable annotations, NonNull annotations are not necessarily correct.

    • Method Detail

      • get_annotation

        public static String get_annotation​(PptTopLevel ppt,
                                    VarInfo vi)
        Get the annotation for the specified variable. Returns @Nullable if samples were found for this variable and at least one sample contained a null value. Returns an (interned) empty string if no annotation is applicable. Otherwise, the return value contains a trailing space.

      • process_method

        public static void process_method​(PptTopLevel ppt)
        Print out the annotations for the specified method.

      • process_obj_fields

        public static void process_obj_fields​(PptTopLevel ppt)
        Print out the annotations for each field in the object or class.

      • field_name

        public static String field_name​(VarInfo vi)
        Returns the field name of the specified variable. This is the relative name for instance fields, but the relative name is not specified for static fields (because there is no enclosing variable with the full name). The field name is obtained in that case, by removing the package/class specifier.

      • is_static_method

        @Pure
public static boolean is_static_method​(PptTopLevel ppt)
        Returns whether or not the method of the specified ppt is static or not. The ppt must be an exit ppt. Exit ppts that do not have an object as a parent are inferred to be static. This does not work for enter ppts, because constructors do not have the object as a parent on entry.