daikon
Class AnnotateNullable

Object
  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.

Field Summary

static boolean	nonnull_annotations Adds NonNull annotations as well as Nullable annotations.
static boolean	stub_format Write an output file in the stub class format (see the Checker Framework Manual), instead of in annotation file format.

Constructor Summary

AnnotateNullable()

Method Summary

static String	field_name(VarInfo vi) Returns the field name of the specified variable.
static String	get_annotation(PptTopLevel ppt, VarInfo vi) Get the annotation for the specified variable.
static boolean	is_static_method(PptTopLevel ppt) Returns whether or not the method of the specified ppt is static or not.
static String	jvm_signature(PptTopLevel ppt) Returns a JVM signature for the method.
static void	main(String[] args)
static void	process_class(PptTopLevel object_ppt)
static void	process_method(PptTopLevel ppt) Print out the annotations for the specified method.
static void	process_obj_fields(PptTopLevel ppt) Print out the annotations for each field in the object or class.

Methods inherited from class Object

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

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.

Constructor Detail

AnnotateNullable

public AnnotateNullable()

Method Detail

main

public static void main(String[] args)
                 throws IOException

Throws:

IOException

process_class

public static void process_class(PptTopLevel object_ppt)

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 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.

jvm_signature

public static String jvm_signature(PptTopLevel ppt)

Returns a JVM signature for the method.

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

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.