Class IndexFileWriter

java.lang.Object
org.checkerframework.afu.scenelib.io.IndexFileWriter

public final class IndexFileWriter extends Object
IndexFileWriter provides two static methods named write that write a given AScene to a given Writer or filename, in index file format.
  • Method Details

    • formatAnnotationValue

      @Deprecated public static String formatAnnotationValue(AnnotationFieldType aft, Object o)
      Deprecated.
      Formats a literal argument of an annotation. Public to permit re-use in stub-based whole-program inference.
      Parameters:
      aft - the type of the annotation field
      o - the value or values to format
      Returns:
      the String representation of the value
    • formatAnnotationValue

      public static void formatAnnotationValue(StringBuilder sb, AnnotationFieldType aft, Object o)
      Formats a literal argument of an annotation. Public to permit re-use in stub-based whole-program inference.
      Parameters:
      sb - where to format the arguments to
      aft - the type of the annotation field
      o - the value or values to format
    • write

      public static void write(AScene scene, Writer out) throws DefException
      Writes the annotations in scene and their definitions to out in index file format.

      An AScene can contain several annotations of the same type but different definitions, while an index file can accommodate only a single definition for each annotation type. This has two consequences:

      • Before writing anything, this method uses a DefCollector to ensure that all definitions of each annotation type are identical (modulo unknown array types). If not, a DefException is thrown.
      • There is one case in which, even if a scene is written successfully, reading it back in produces a different scene. Consider a scene containing two annotations of type Foo, each with an array field bar. In one annotation, bar is empty and of unknown element type (see AnnotationBuilder.addEmptyArrayField(java.lang.String)); in the other, bar is of known element type. This method will unify the two definitions of Foo by writing a single definition with known element type. When the index file is read into a new scene, the definitions of both annotations will have known element type, whereas in the original scene, one had unknown element type.
      Throws:
      DefException
    • write

      public static void write(AScene scene, String filename) throws IOException, DefException
      Writes the annotations in scene and their definitions to the file filename in index file format; see write(AScene, Writer).
      Throws:
      IOException
      DefException